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

Theorem simpl13 1249
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 1192 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜒)
213ad2antl1 1184 1 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 207  df-an 396  df-3an 1088
This theorem is referenced by:  pythagtriplem4  16853  mply1topmatcl  22827  nolt02o  27755  nogt01o  27756  cofsslt  27967  coinitsslt  27968  brbtwn2  28935  ax5seg  28968  br8  35736  btwndiff  36009  ifscgr  36026  seglecgr12im  36092  atlatle  39302  cvlcvr1  39321  atbtwn  39429  3dimlem3  39444  3dimlem3OLDN  39445  4atlem3  39579  4atlem11  39592  4atlem12  39595  2lplnj  39603  paddasslem4  39806  paddasslem10  39812  pmodlem1  39829  llnexchb2lem  39851  pclfinclN  39933  arglem1N  40173  cdlemd4  40184  cdlemd  40190  cdleme16  40268  cdleme20  40307  cdleme21k  40321  cdleme22cN  40325  cdleme27N  40352  cdleme28c  40355  cdleme29ex  40357  cdleme32fva  40420  cdleme40n  40451  cdlemg15a  40638  cdlemg15  40639  cdlemg16ALTN  40641  cdlemg16z  40642  cdlemg20  40668  cdlemg22  40670  cdlemg29  40688  cdlemg38  40698  cdlemk56  40954  dihord2pre  41208  ismnu  44257  uzwo4  44993  fourierdlem77  46139
  Copyright terms: Public domain W3C validator