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

Theorem simpl13 1319
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 1232 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜒)
213ad2antl1 1201 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  15726  mply1topmatcl  20812  brbtwn2  25984  ax5seg  26017  br8  31953  nolt02o  32151  btwndiff  32440  ifscgr  32457  seglecgr12im  32523  atlatle  35110  cvlcvr1  35129  atbtwn  35235  3dimlem3  35250  3dimlem3OLDN  35251  4atlem3  35385  4atlem11  35398  4atlem12  35401  2lplnj  35409  paddasslem4  35612  paddasslem10  35618  pmodlem1  35635  llnexchb2lem  35657  pclfinclN  35739  arglem1N  35980  cdlemd4  35991  cdlemd  35997  cdleme16  36075  cdleme20  36114  cdleme21k  36128  cdleme22cN  36132  cdleme27N  36159  cdleme28c  36162  cdleme29ex  36164  cdleme32fva  36227  cdleme40n  36258  cdlemg15a  36445  cdlemg15  36446  cdlemg16ALTN  36448  cdlemg16z  36449  cdlemg20  36475  cdlemg22  36477  cdlemg29  36495  cdlemg38  36505  cdlemk56  36761  dihord2pre  37016  uzwo4  39720  fourierdlem77  40903
  Copyright terms: Public domain W3C validator