MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpl3r Structured version   Visualization version   GIF version

Theorem simpl3r 1137
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpl3r (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)

Proof of Theorem simpl3r
StepHypRef Expression
1 simp3r 1110 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜓)
21adantr 480 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1056
This theorem is referenced by:  tfisi  7100  omopth2  7709  ltmul1a  10910  xmulasslem3  12154  xadddi2  12165  swrdsbslen  13494  swrdspsleq  13495  dvdsadd2b  15075  pockthg  15657  psgnunilem4  17963  efgred  18207  marrepeval  20417  submaeval  20436  mdetmul  20477  minmar1eval  20503  ptbasin  21428  basqtop  21562  xrsmopn  22662  axpasch  25866  axeuclid  25888  elwwlks2ons3im  26919  br4  31774  nosupbnd1lem3  31981  nosupbnd1lem4  31982  nosupbnd1lem5  31983  btwnouttr2  32254  trisegint  32260  cgrxfr  32287  lineext  32308  btwnconn1lem13  32331  btwnconn1lem14  32332  btwnconn3  32335  brsegle  32340  brsegle2  32341  segleantisym  32347  outsideofeu  32363  lineunray  32379  lineelsb2  32380  cvrcmp  34888  atcvrj2b  35036  3dimlem3  35065  3dimlem3OLDN  35066  3dim3  35073  ps-1  35081  ps-2  35082  lplnnle2at  35145  2llnm3N  35173  4atlem0a  35197  4atlem3  35200  4atlem3a  35201  lnatexN  35383  paddasslem8  35431  paddasslem9  35432  paddasslem10  35433  paddasslem12  35435  paddasslem13  35436  lhpexle2lem  35613  lhpexle3  35616  lhpat3  35650  4atex  35680  trlval2  35768  trlval4  35793  cdleme16  35890  cdleme21  35942  cdleme21k  35943  cdleme27cl  35971  cdleme27N  35974  cdleme43fsv1snlem  36025  cdleme48fvg  36105  cdlemg8  36236  cdlemg15a  36260  cdlemg16z  36264  cdlemg24  36293  cdlemg38  36320  cdlemg40  36322  trlcone  36333  cdlemj2  36427  tendoid0  36430  tendoconid  36434  cdlemk34  36515  cdlemk38  36520  cdlemkid4  36539  cdlemk53  36562  tendospcanN  36629  dihvalcqpre  36841  dihmeetlem15N  36927  qirropth  37790  mzpcong  37856  jm2.26  37886  aomclem6  37946  islptre  40169  limccog  40170  limcleqr  40194  fourierdlem42  40684  elaa2  40769
  Copyright terms: Public domain W3C validator