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

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

Proof of Theorem simp13r
StepHypRef Expression
1 simp3r 1245 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant1 1128 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  pceu  15753  axpasch  26020  3dimlem4  35253  3atlem4  35275  llncvrlpln2  35346  2lplnja  35408  lhpmcvr5N  35816  4atexlemswapqr  35852  4atexlemnclw  35859  trlval2  35953  cdleme21h  36124  cdleme24  36142  cdleme26ee  36150  cdleme26f  36153  cdleme26f2  36155  cdlemf1  36351  cdlemg16ALTN  36448  cdlemg17iqN  36464  cdlemg27b  36486  trlcone  36518  cdlemg48  36527  tendocan  36614  cdlemk26-3  36696  cdlemk27-3  36697  cdlemk28-3  36698  cdlemk37  36704  cdlemky  36716  cdlemk11ta  36719  cdlemkid3N  36723  cdlemk11t  36736  cdlemk46  36738  cdlemk47  36739  cdlemk51  36743  cdlemk52  36744  cdleml4N  36769  dihmeetlem1N  37081  dihmeetlem20N  37117  mapdpglem32  37496  addlimc  40383
  Copyright terms: Public domain W3C validator