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

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

Proof of Theorem simp33l
StepHypRef Expression
1 simp3l 1243 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant3 1129 1 ((𝜏𝜂 ∧ (𝜒𝜃 ∧ (𝜑𝜓))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  totprob  30829  cdleme19b  36113  cdleme19d  36115  cdleme19e  36116  cdleme20h  36125  cdleme20l2  36130  cdleme20m  36132  cdleme21d  36139  cdleme21e  36140  cdleme22e  36153  cdleme22f2  36156  cdleme22g  36157  cdleme26e  36168  cdleme28a  36179  cdleme28b  36180  cdleme37m  36271  cdleme39n  36275  cdlemeg46gfre  36341  cdlemg28a  36502  cdlemg28b  36512  cdlemk3  36642  cdlemk5a  36644  cdlemk6  36646  cdlemkuat  36675  cdlemkid2  36733
  Copyright terms: Public domain W3C validator