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

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

Proof of Theorem simp33r
StepHypRef Expression
1 simp3r 1252 . 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:  totprob  30808  cdleme19b  36079  cdleme19e  36082  cdleme20h  36091  cdleme20l2  36096  cdleme20m  36098  cdleme21d  36105  cdleme21e  36106  cdleme22eALTN  36120  cdleme22f2  36122  cdleme22g  36123  cdleme26e  36134  cdleme37m  36237  cdlemeg46gfre  36307  cdlemg28a  36468  cdlemg28b  36478  cdlemk5a  36610  cdlemk6  36612
  Copyright terms: Public domain W3C validator