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

Theorem simpl13 1244
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 1187 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜒)
213ad2antl1 1179 1 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  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 208  df-an 397  df-3an 1083
This theorem is referenced by:  pythagtriplem4  16146  mply1topmatcl  21329  brbtwn2  26605  ax5seg  26638  br8  32876  nolt02o  33083  btwndiff  33372  ifscgr  33389  seglecgr12im  33455  atlatle  36323  cvlcvr1  36342  atbtwn  36449  3dimlem3  36464  3dimlem3OLDN  36465  4atlem3  36599  4atlem11  36612  4atlem12  36615  2lplnj  36623  paddasslem4  36826  paddasslem10  36832  pmodlem1  36849  llnexchb2lem  36871  pclfinclN  36953  arglem1N  37193  cdlemd4  37204  cdlemd  37210  cdleme16  37288  cdleme20  37327  cdleme21k  37341  cdleme22cN  37345  cdleme27N  37372  cdleme28c  37375  cdleme29ex  37377  cdleme32fva  37440  cdleme40n  37471  cdlemg15a  37658  cdlemg15  37659  cdlemg16ALTN  37661  cdlemg16z  37662  cdlemg20  37688  cdlemg22  37690  cdlemg29  37708  cdlemg38  37718  cdlemk56  37974  dihord2pre  38228  ismnu  40462  uzwo4  41180  fourierdlem77  42334
  Copyright terms: Public domain W3C validator