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

Theorem simpl13 1337
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 1250 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜒)
213ad2antl1 1240 1 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1111
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 199  df-an 387  df-3an 1113
This theorem is referenced by:  pythagtriplem4  15895  mply1topmatcl  20980  brbtwn2  26204  ax5seg  26237  br8  32177  nolt02o  32373  btwndiff  32662  ifscgr  32679  seglecgr12im  32745  atlatle  35388  cvlcvr1  35407  atbtwn  35514  3dimlem3  35529  3dimlem3OLDN  35530  4atlem3  35664  4atlem11  35677  4atlem12  35680  2lplnj  35688  paddasslem4  35891  paddasslem10  35897  pmodlem1  35914  llnexchb2lem  35936  pclfinclN  36018  arglem1N  36258  cdlemd4  36269  cdlemd  36275  cdleme16  36353  cdleme20  36392  cdleme21k  36406  cdleme22cN  36410  cdleme27N  36437  cdleme28c  36440  cdleme29ex  36442  cdleme32fva  36505  cdleme40n  36536  cdlemg15a  36723  cdlemg15  36724  cdlemg16ALTN  36726  cdlemg16z  36727  cdlemg20  36753  cdlemg22  36755  cdlemg29  36773  cdlemg38  36783  cdlemk56  37039  dihord2pre  37293  uzwo4  40031  fourierdlem77  41187
  Copyright terms: Public domain W3C validator