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

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

Proof of Theorem simpl21
StepHypRef Expression
1 simp21 1092 . 2 ((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) → 𝜑)
21adantr 481 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  brbtwn2  25702  ax5seglem3a  25727  ax5seg  25735  axpasch  25738  axeuclid  25760  br8d  29288  br8  31389  cgrextend  31792  segconeq  31794  trisegint  31812  ifscgr  31828  cgrsub  31829  cgrxfr  31839  lineext  31860  seglecgr12im  31894  segletr  31898  lineunray  31931  lineelsb2  31932  cvrcmp  34085  cvlatexch3  34140  cvlsupr2  34145  atexchcvrN  34241  3dim1  34268  3dim2  34269  ps-1  34278  ps-2  34279  3atlem3  34286  3atlem5  34288  lplnnle2at  34342  lplnllnneN  34357  2llnjaN  34367  4atlem3  34397  4atlem10b  34406  4atlem12  34413  2llnma3r  34589  paddasslem4  34624  paddasslem7  34627  paddasslem8  34628  paddasslem12  34632  paddasslem13  34633  pmodlem1  34647  pmodlem2  34648  llnexchb2lem  34669  4atex2  34878  ltrnatlw  34985  trlval4  34990  arglem1N  34992  cdlemd4  35003  cdlemd5  35004  cdleme0moN  35027  cdleme16  35087  cdleme20  35127  cdleme21j  35139  cdleme21k  35141  cdleme27N  35172  cdleme28c  35175  cdleme43fsv1snlem  35223  cdleme38n  35267  cdleme40n  35271  cdleme41snaw  35279  cdlemg6c  35423  cdlemg8c  35432  cdlemg8  35434  cdlemg12e  35450  cdlemg16  35460  cdlemg16ALTN  35461  cdlemg16z  35462  cdlemg16zz  35463  cdlemg18a  35481  cdlemg20  35488  cdlemg22  35490  cdlemg37  35492  cdlemg27b  35499  cdlemg31d  35503  cdlemg33  35514  cdlemg38  35518  cdlemg44b  35535  cdlemk38  35718  cdlemk35s-id  35741  cdlemk39s-id  35743  cdlemk55  35764  cdlemk35u  35767  cdlemk55u  35769  cdleml3N  35781  cdlemn11pre  36014
  Copyright terms: Public domain W3C validator