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

Theorem simpl13 1333
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 1246 . 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  15805  mply1topmatcl  20889  brbtwn2  26076  ax5seg  26109  br8  32023  nolt02o  32221  btwndiff  32510  ifscgr  32527  seglecgr12im  32593  atlatle  35208  cvlcvr1  35227  atbtwn  35334  3dimlem3  35349  3dimlem3OLDN  35350  4atlem3  35484  4atlem11  35497  4atlem12  35500  2lplnj  35508  paddasslem4  35711  paddasslem10  35717  pmodlem1  35734  llnexchb2lem  35756  pclfinclN  35838  arglem1N  36078  cdlemd4  36089  cdlemd  36095  cdleme16  36173  cdleme20  36212  cdleme21k  36226  cdleme22cN  36230  cdleme27N  36257  cdleme28c  36260  cdleme29ex  36262  cdleme32fva  36325  cdleme40n  36356  cdlemg15a  36543  cdlemg15  36544  cdlemg16ALTN  36546  cdlemg16z  36547  cdlemg20  36573  cdlemg22  36575  cdlemg29  36593  cdlemg38  36603  cdlemk56  36859  dihord2pre  37113  uzwo4  39804  fourierdlem77  40969
  Copyright terms: Public domain W3C validator