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

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

Proof of Theorem simp13r
StepHypRef Expression
1 simp3r 1203 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant1 1134 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  pceu  16884  axpasch  28956  3dimlem4  39466  3atlem4  39488  llncvrlpln2  39559  2lplnja  39621  lhpmcvr5N  40029  4atexlemswapqr  40065  4atexlemnclw  40072  trlval2  40165  cdleme21h  40336  cdleme24  40354  cdleme26ee  40362  cdleme26f  40365  cdleme26f2  40367  cdlemf1  40563  cdlemg16ALTN  40660  cdlemg17iqN  40676  cdlemg27b  40698  trlcone  40730  cdlemg48  40739  tendocan  40826  cdlemk26-3  40908  cdlemk27-3  40909  cdlemk28-3  40910  cdlemk37  40916  cdlemky  40928  cdlemk11ta  40931  cdlemkid3N  40935  cdlemk11t  40948  cdlemk46  40950  cdlemk47  40951  cdlemk51  40955  cdlemk52  40956  cdleml4N  40981  dihmeetlem1N  41292  dihmeetlem20N  41328  mapdpglem32  41707  addlimc  45663  iscnrm3rlem8  48844
  Copyright terms: Public domain W3C validator