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

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

Proof of Theorem simp33l
StepHypRef Expression
1 simp3l 1082 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant3 1077 1 ((𝜏𝜂 ∧ (𝜒𝜃 ∧ (𝜑𝜓))) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  totprob  29816  cdleme19b  34610  cdleme19d  34612  cdleme19e  34613  cdleme20h  34622  cdleme20l2  34627  cdleme20m  34629  cdleme21d  34636  cdleme21e  34637  cdleme22e  34650  cdleme22f2  34653  cdleme22g  34654  cdleme26e  34665  cdleme28a  34676  cdleme28b  34677  cdleme37m  34768  cdleme39n  34772  cdlemeg46gfre  34838  cdlemg28a  34999  cdlemg28b  35009  cdlemk3  35139  cdlemk5a  35141  cdlemk6  35143  cdlemkuat  35172  cdlemkid2  35230
 Copyright terms: Public domain W3C validator