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

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

Proof of Theorem simp21r
StepHypRef Expression
1 simp1r 1194 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
213ad2ant2 1130 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1083
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 209  df-an 399  df-3an 1085
This theorem is referenced by:  modexp  13582  segconeu  33477  4atlem10  36775  lplncvrlvol2  36784  4atex  37245  4atex2-0cOLDN  37249  cdleme0moN  37394  cdleme16e  37451  cdleme17d1  37458  cdleme18d  37464  cdleme19d  37475  cdleme20f  37483  cdleme20g  37484  cdleme21ct  37498  cdleme22aa  37508  cdleme22cN  37511  cdleme22d  37512  cdleme22e  37513  cdleme22eALTN  37514  cdleme26e  37528  cdleme32e  37614  cdleme32f  37615  cdlemg4  37786  cdlemg18d  37850  cdlemg18  37851  cdlemg19a  37852  cdlemg19  37853  cdlemg21  37855  cdlemg33b0  37870  cdlemk5  38005  cdlemk6  38006  cdlemk7  38017  cdlemk11  38018  cdlemk12  38019  cdlemk21N  38042  cdlemk20  38043  cdlemk28-3  38077  cdlemk34  38079  cdlemkfid3N  38094  cdlemk55u1  38134
  Copyright terms: Public domain W3C validator