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

Theorem simpl12 1331
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 1244 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜓)
213ad2antl1 1236 1 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 1109
This theorem is referenced by:  pythagtriplem4  15803  pmatcollpw1lem1  20858  pmatcollpw1  20860  mp2pm2mplem2  20891  brbtwn2  26076  ax5seg  26109  3vfriswmgr  27558  br8  32091  nolt02o  32289  ifscgr  32595  seglecgr12im  32661  lkrshp  35061  atlatle  35276  cvlcvr1  35295  atbtwn  35402  3dimlem3  35417  3dimlem3OLDN  35418  1cvratex  35429  llnmlplnN  35495  4atlem3  35552  4atlem3a  35553  4atlem11  35565  4atlem12  35568  cdlemb  35750  paddasslem4  35779  paddasslem10  35785  pmodlem1  35802  llnexchb2lem  35824  arglem1N  36146  cdlemd4  36157  cdlemd  36163  cdleme16  36241  cdleme20  36280  cdleme21k  36294  cdleme22cN  36298  cdleme27N  36325  cdleme28c  36328  cdleme29ex  36330  cdleme32fva  36393  cdleme40n  36424  cdlemg15a  36611  cdlemg15  36612  cdlemg16ALTN  36614  cdlemg16z  36615  cdlemg20  36641  cdlemg22  36643  cdlemg29  36661  cdlemg38  36671  cdlemk33N  36865  cdlemk56  36927  fourierdlem77  41037
  Copyright terms: Public domain W3C validator