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

Theorem simpl12 1243
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 1186 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜓)
213ad2antl1 1179 1 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1081
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 209  df-an 399  df-3an 1083
This theorem is referenced by:  pythagtriplem4  16148  pmatcollpw1lem1  21374  pmatcollpw1  21376  mp2pm2mplem2  21407  brbtwn2  26683  ax5seg  26716  3vfriswmgr  28049  br8  32980  nolt02o  33187  ifscgr  33493  seglecgr12im  33559  lkrshp  36228  atlatle  36443  cvlcvr1  36462  atbtwn  36569  3dimlem3  36584  3dimlem3OLDN  36585  1cvratex  36596  llnmlplnN  36662  4atlem3  36719  4atlem3a  36720  4atlem11  36732  4atlem12  36735  cdlemb  36917  paddasslem4  36946  paddasslem10  36952  pmodlem1  36969  llnexchb2lem  36991  arglem1N  37313  cdlemd4  37324  cdlemd  37330  cdleme16  37408  cdleme20  37447  cdleme21k  37461  cdleme22cN  37465  cdleme27N  37492  cdleme28c  37495  cdleme29ex  37497  cdleme32fva  37560  cdleme40n  37591  cdlemg15a  37778  cdlemg15  37779  cdlemg16ALTN  37781  cdlemg16z  37782  cdlemg20  37808  cdlemg22  37810  cdlemg29  37828  cdlemg38  37838  cdlemk33N  38032  cdlemk56  38094  fourierdlem77  42453
  Copyright terms: Public domain W3C validator