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

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

Proof of Theorem simpl13
StepHypRef Expression
1 simpl3 1185 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜒)
213ad2antl1 1177 1 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  pythagtriplem4  16146  mply1topmatcl  21343  brbtwn2  26619  ax5seg  26652  br8  32890  nolt02o  33097  btwndiff  33386  ifscgr  33403  seglecgr12im  33469  atlatle  36338  cvlcvr1  36357  atbtwn  36464  3dimlem3  36479  3dimlem3OLDN  36480  4atlem3  36614  4atlem11  36627  4atlem12  36630  2lplnj  36638  paddasslem4  36841  paddasslem10  36847  pmodlem1  36864  llnexchb2lem  36886  pclfinclN  36968  arglem1N  37208  cdlemd4  37219  cdlemd  37225  cdleme16  37303  cdleme20  37342  cdleme21k  37356  cdleme22cN  37360  cdleme27N  37387  cdleme28c  37390  cdleme29ex  37392  cdleme32fva  37455  cdleme40n  37486  cdlemg15a  37673  cdlemg15  37674  cdlemg16ALTN  37676  cdlemg16z  37677  cdlemg20  37703  cdlemg22  37705  cdlemg29  37723  cdlemg38  37733  cdlemk56  37989  dihord2pre  38243  ismnu  40477  uzwo4  41195  fourierdlem77  42349
  Copyright terms: Public domain W3C validator