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

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

Proof of Theorem simpl21
StepHypRef Expression
1 simpl1 1235 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜑)
213ad2antl2 1230 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  brbtwn2  26009  ax5seglem3a  26034  ax5seg  26042  axpasch  26045  axeuclid  26067  br8d  29757  br8  31977  nosupbnd2lem1  32191  cgrextend  32445  segconeq  32447  trisegint  32465  ifscgr  32481  cgrsub  32482  cgrxfr  32492  lineext  32513  seglecgr12im  32547  segletr  32551  lineunray  32584  lineelsb2  32585  cvrcmp  35069  cvlatexch3  35124  cvlsupr2  35129  atexchcvrN  35226  3dim1  35253  3dim2  35254  ps-1  35263  ps-2  35264  3atlem3  35271  3atlem5  35273  lplnnle2at  35327  lplnllnneN  35342  2llnjaN  35352  4atlem3  35382  4atlem10b  35391  4atlem12  35398  2llnma3r  35574  paddasslem4  35609  paddasslem7  35612  paddasslem8  35613  paddasslem12  35617  paddasslem13  35618  pmodlem1  35632  pmodlem2  35633  llnexchb2lem  35654  4atex2  35863  ltrnatlw  35969  trlval4  35974  arglem1N  35976  cdlemd4  35987  cdlemd5  35988  cdleme0moN  36011  cdleme16  36071  cdleme20  36110  cdleme21j  36122  cdleme21k  36124  cdleme27N  36155  cdleme28c  36158  cdleme43fsv1snlem  36206  cdleme38n  36250  cdleme40n  36254  cdleme41snaw  36262  cdlemg6c  36406  cdlemg8c  36415  cdlemg8  36417  cdlemg12e  36433  cdlemg16  36443  cdlemg16ALTN  36444  cdlemg16z  36445  cdlemg16zz  36446  cdlemg18a  36464  cdlemg20  36471  cdlemg22  36473  cdlemg37  36475  cdlemg27b  36482  cdlemg31d  36486  cdlemg33  36497  cdlemg38  36501  cdlemg44b  36518  cdlemk38  36701  cdlemk35s-id  36724  cdlemk39s-id  36726  cdlemk55  36747  cdlemk35u  36750  cdlemk55u  36752  cdleml3N  36764  cdlemn11pre  36996
  Copyright terms: Public domain W3C validator