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

Theorem simpl22 1252
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)
Assertion
Ref Expression
simpl22 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem simpl22
StepHypRef Expression
1 simpl2 1192 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜓)
213ad2antl2 1186 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  brbtwn2  27683  ax5seg  27716  axpasch  27719  axeuclid  27741  br8d  31358  br8  34145  cgrextend  34531  segconeq  34533  trisegint  34551  ifscgr  34567  cgrsub  34568  cgrxfr  34578  lineext  34599  seglecgr12im  34633  segletr  34637  lineunray  34670  lineelsb2  34671  cvrcmp  37683  cvlatexch3  37738  cvlsupr2  37743  atcvrj2b  37833  atexchcvrN  37841  3dim1  37868  3dim2  37869  3atlem3  37886  3atlem5  37888  lplnnle2at  37942  2llnjaN  37967  4atlem3  37997  4atlem10b  38006  4atlem12  38013  2llnma3r  38189  paddasslem4  38224  paddasslem7  38227  paddasslem8  38228  paddasslem12  38232  paddasslem13  38233  paddasslem15  38235  pmodlem1  38247  pmodlem2  38248  atmod1i1m  38259  llnexchb2lem  38269  4atex2  38478  ltrnatlw  38584  trlval4  38589  arglem1N  38591  cdlemd4  38602  cdlemd5  38603  cdleme0moN  38626  cdleme16  38686  cdleme20  38725  cdleme21k  38739  cdleme27N  38770  cdleme28c  38773  cdleme43fsv1snlem  38821  cdleme38n  38865  cdleme40n  38869  cdleme41snaw  38877  cdlemg6c  39021  cdlemg8c  39030  cdlemg8  39032  cdlemg12e  39048  cdlemg16  39058  cdlemg16ALTN  39059  cdlemg16z  39060  cdlemg16zz  39061  cdlemg18a  39079  cdlemg20  39086  cdlemg22  39088  cdlemg37  39090  cdlemg31d  39101  cdlemg33  39112  cdlemg38  39116  cdlemg44b  39133  cdlemk38  39316  cdlemk35s-id  39339  cdlemk39s-id  39341  cdlemk53b  39357  cdlemk55  39362  cdlemk35u  39365  cdlemk55u  39367  cdlemn11pre  39611
  Copyright terms: Public domain W3C validator