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

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

Proof of Theorem simp13r
StepHypRef Expression
1 simp3r 1199 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant1 1130 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084
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 206  df-an 395  df-3an 1086
This theorem is referenced by:  pceu  16841  axpasch  28870  3dimlem4  39174  3atlem4  39196  llncvrlpln2  39267  2lplnja  39329  lhpmcvr5N  39737  4atexlemswapqr  39773  4atexlemnclw  39780  trlval2  39873  cdleme21h  40044  cdleme24  40062  cdleme26ee  40070  cdleme26f  40073  cdleme26f2  40075  cdlemf1  40271  cdlemg16ALTN  40368  cdlemg17iqN  40384  cdlemg27b  40406  trlcone  40438  cdlemg48  40447  tendocan  40534  cdlemk26-3  40616  cdlemk27-3  40617  cdlemk28-3  40618  cdlemk37  40624  cdlemky  40636  cdlemk11ta  40639  cdlemkid3N  40643  cdlemk11t  40656  cdlemk46  40658  cdlemk47  40659  cdlemk51  40663  cdlemk52  40664  cdleml4N  40689  dihmeetlem1N  41000  dihmeetlem20N  41036  mapdpglem32  41415  addlimc  45303  iscnrm3rlem8  48315
  Copyright terms: Public domain W3C validator