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

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

Proof of Theorem simpl12
StepHypRef Expression
1 simpl2 1206 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜓)
213ad2antl1 1177 1 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  pythagtriplem4  15697  pmatcollpw1lem1  20752  pmatcollpw1  20754  mp2pm2mplem2  20785  brbtwn2  25955  ax5seg  25988  3vfriswmgr  27403  br8  31924  nolt02o  32122  ifscgr  32428  seglecgr12im  32494  lkrshp  34864  atlatle  35079  cvlcvr1  35098  atbtwn  35204  3dimlem3  35219  3dimlem3OLDN  35220  1cvratex  35231  llnmlplnN  35297  4atlem3  35354  4atlem3a  35355  4atlem11  35367  4atlem12  35370  cdlemb  35552  paddasslem4  35581  paddasslem10  35587  pmodlem1  35604  llnexchb2lem  35626  arglem1N  35949  cdlemd4  35960  cdlemd  35966  cdleme16  36044  cdleme20  36083  cdleme21k  36097  cdleme22cN  36101  cdleme27N  36128  cdleme28c  36131  cdleme29ex  36133  cdleme32fva  36196  cdleme40n  36227  cdlemg15a  36414  cdlemg15  36415  cdlemg16ALTN  36417  cdlemg16z  36418  cdlemg20  36444  cdlemg22  36446  cdlemg29  36464  cdlemg38  36474  cdlemk33N  36668  cdlemk56  36730  fourierdlem77  40872
  Copyright terms: Public domain W3C validator