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

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

Proof of Theorem simp13r
StepHypRef Expression
1 simp3r 1216 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant1 1124 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1071
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 199  df-an 387  df-3an 1073
This theorem is referenced by:  pceu  15955  axpasch  26290  3dimlem4  35613  3atlem4  35635  llncvrlpln2  35706  2lplnja  35768  lhpmcvr5N  36176  4atexlemswapqr  36212  4atexlemnclw  36219  trlval2  36312  cdleme21h  36483  cdleme24  36501  cdleme26ee  36509  cdleme26f  36512  cdleme26f2  36514  cdlemf1  36710  cdlemg16ALTN  36807  cdlemg17iqN  36823  cdlemg27b  36845  trlcone  36877  cdlemg48  36886  tendocan  36973  cdlemk26-3  37055  cdlemk27-3  37056  cdlemk28-3  37057  cdlemk37  37063  cdlemky  37075  cdlemk11ta  37078  cdlemkid3N  37082  cdlemk11t  37095  cdlemk46  37097  cdlemk47  37098  cdlemk51  37102  cdlemk52  37103  cdleml4N  37128  dihmeetlem1N  37439  dihmeetlem20N  37475  mapdpglem32  37854  addlimc  40781
  Copyright terms: Public domain W3C validator