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

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

Proof of Theorem simp21r
StepHypRef Expression
1 simp1r 1239 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
213ad2ant2 1127 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1070
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 1072
This theorem is referenced by:  modexp  13205  segconeu  32449  4atlem10  35407  lplncvrlvol2  35416  4atex  35877  4atex2-0cOLDN  35881  cdleme0moN  36027  cdleme16e  36084  cdleme17d1  36091  cdleme18d  36097  cdleme19d  36108  cdleme20f  36116  cdleme20g  36117  cdleme21ct  36131  cdleme22aa  36141  cdleme22cN  36144  cdleme22d  36145  cdleme22e  36146  cdleme22eALTN  36147  cdleme26e  36161  cdleme32e  36247  cdleme32f  36248  cdlemg4  36419  cdlemg18d  36483  cdlemg18  36484  cdlemg19a  36485  cdlemg19  36486  cdlemg21  36488  cdlemg33b0  36503  cdlemk5  36638  cdlemk6  36639  cdlemk7  36650  cdlemk11  36651  cdlemk12  36652  cdlemk21N  36675  cdlemk20  36676  cdlemk28-3  36710  cdlemk34  36712  cdlemkfid3N  36727  cdlemk55u1  36767
  Copyright terms: Public domain W3C validator