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

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

Proof of Theorem simp32l
StepHypRef Expression
1 simp2l 1249 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
213ad2ant3 1158 1 ((𝜏𝜂 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  cdlema1N  35590  paddasslem15  35633  4atex2-0aOLDN  35877  4atex3  35880  trlval3  35986  cdleme12  36070  cdleme19b  36103  cdleme19d  36105  cdleme19e  36106  cdleme20d  36111  cdleme20f  36113  cdleme20g  36114  cdleme21d  36129  cdleme21e  36130  cdleme21f  36131  cdleme22cN  36141  cdleme22e  36143  cdleme22f2  36146  cdleme22g  36147  cdleme26e  36158  cdleme28a  36169  cdleme37m  36261  cdleme39n  36265  cdlemg28b  36502  cdlemk3  36632  cdlemk12  36649  cdlemk12u  36671  cdlemkoatnle-2N  36674  cdlemk13-2N  36675  cdlemkole-2N  36676  cdlemk14-2N  36677  cdlemk15-2N  36678  cdlemk16-2N  36679  cdlemk17-2N  36680  cdlemk18-2N  36685  cdlemk19-2N  36686  cdlemk7u-2N  36687  cdlemk11u-2N  36688  cdlemk20-2N  36691  cdlemk30  36693  cdlemk23-3  36701  cdlemk24-3  36702
  Copyright terms: Public domain W3C validator