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

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

Proof of Theorem simp13r
StepHypRef Expression
1 simp3r 1204 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant1 1135 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089
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 210  df-an 400  df-3an 1091
This theorem is referenced by:  pceu  16431  axpasch  27063  3dimlem4  37251  3atlem4  37273  llncvrlpln2  37344  2lplnja  37406  lhpmcvr5N  37814  4atexlemswapqr  37850  4atexlemnclw  37857  trlval2  37950  cdleme21h  38121  cdleme24  38139  cdleme26ee  38147  cdleme26f  38150  cdleme26f2  38152  cdlemf1  38348  cdlemg16ALTN  38445  cdlemg17iqN  38461  cdlemg27b  38483  trlcone  38515  cdlemg48  38524  tendocan  38611  cdlemk26-3  38693  cdlemk27-3  38694  cdlemk28-3  38695  cdlemk37  38701  cdlemky  38713  cdlemk11ta  38716  cdlemkid3N  38720  cdlemk11t  38733  cdlemk46  38735  cdlemk47  38736  cdlemk51  38740  cdlemk52  38741  cdleml4N  38766  dihmeetlem1N  39077  dihmeetlem20N  39113  mapdpglem32  39492  addlimc  42909  iscnrm3rlem8  45959
  Copyright terms: Public domain W3C validator