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

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

Proof of Theorem simpl22
StepHypRef Expression
1 simp22 1093 . 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  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  atcvrj2b  34233  atexchcvrN  34241  3dim1  34268  3dim2  34269  3atlem3  34286  3atlem5  34288  lplnnle2at  34342  2llnjaN  34367  4atlem3  34397  4atlem10b  34406  4atlem12  34413  2llnma3r  34589  paddasslem4  34624  paddasslem7  34627  paddasslem8  34628  paddasslem12  34632  paddasslem13  34633  paddasslem15  34635  pmodlem1  34647  pmodlem2  34648  atmod1i1m  34659  llnexchb2lem  34669  4atex2  34878  ltrnatlw  34985  trlval4  34990  arglem1N  34992  cdlemd4  35003  cdlemd5  35004  cdleme0moN  35027  cdleme16  35087  cdleme20  35127  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  cdlemg31d  35503  cdlemg33  35514  cdlemg38  35518  cdlemg44b  35535  cdlemk38  35718  cdlemk35s-id  35741  cdlemk39s-id  35743  cdlemk53b  35759  cdlemk55  35764  cdlemk35u  35767  cdlemk55u  35769  cdlemn11pre  36014
  Copyright terms: Public domain W3C validator