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

Theorem simp33l 1400
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp33l ((𝜏𝜂 ∧ (𝜒𝜃 ∧ (𝜑𝜓))) → 𝜑)

Proof of Theorem simp33l
StepHypRef Expression
1 simp3l 1259 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant3 1166 1 ((𝜏𝜂 ∧ (𝜒𝜃 ∧ (𝜑𝜓))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  w3a 1108
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 386  df-3an 1110
This theorem is referenced by:  totprob  30998  cdleme19b  36317  cdleme19d  36319  cdleme19e  36320  cdleme20h  36329  cdleme20l2  36334  cdleme20m  36336  cdleme21d  36343  cdleme21e  36344  cdleme22e  36357  cdleme22f2  36360  cdleme22g  36361  cdleme26e  36372  cdleme28a  36383  cdleme28b  36384  cdleme37m  36475  cdleme39n  36479  cdlemeg46gfre  36545  cdlemg28a  36706  cdlemg28b  36716  cdlemk3  36846  cdlemk5a  36848  cdlemk6  36850  cdlemkuat  36879  cdlemkid2  36937
  Copyright terms: Public domain W3C validator