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

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

Proof of Theorem simp13r
StepHypRef Expression
1 simp3r 1088 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant1 1080 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  pceu  15470  axpasch  25716  3dimlem4  34216  3atlem4  34238  llncvrlpln2  34309  2lplnja  34371  lhpmcvr5N  34779  4atexlemswapqr  34815  4atexlemnclw  34822  trlval2  34916  cdleme21h  35088  cdleme24  35106  cdleme26ee  35114  cdleme26f  35117  cdleme26f2  35119  cdlemf1  35315  cdlemg16ALTN  35412  cdlemg17iqN  35428  cdlemg27b  35450  trlcone  35482  cdlemg48  35491  tendocan  35578  cdlemk26-3  35660  cdlemk27-3  35661  cdlemk28-3  35662  cdlemk37  35668  cdlemky  35680  cdlemk11ta  35683  cdlemkid3N  35687  cdlemk11t  35700  cdlemk46  35702  cdlemk47  35703  cdlemk51  35707  cdlemk52  35708  cdleml4N  35733  dihmeetlem1N  36045  dihmeetlem20N  36081  mapdpglem32  36460  addlimc  39271
  Copyright terms: Public domain W3C validator