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 399  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 210  df-an 400  df-3an 1086
This theorem is referenced by:  pceu  16160  axpasch  26714  3dimlem4  36646  3atlem4  36668  llncvrlpln2  36739  2lplnja  36801  lhpmcvr5N  37209  4atexlemswapqr  37245  4atexlemnclw  37252  trlval2  37345  cdleme21h  37516  cdleme24  37534  cdleme26ee  37542  cdleme26f  37545  cdleme26f2  37547  cdlemf1  37743  cdlemg16ALTN  37840  cdlemg17iqN  37856  cdlemg27b  37878  trlcone  37910  cdlemg48  37919  tendocan  38006  cdlemk26-3  38088  cdlemk27-3  38089  cdlemk28-3  38090  cdlemk37  38096  cdlemky  38108  cdlemk11ta  38111  cdlemkid3N  38115  cdlemk11t  38128  cdlemk46  38130  cdlemk47  38131  cdlemk51  38135  cdlemk52  38136  cdleml4N  38161  dihmeetlem1N  38472  dihmeetlem20N  38508  mapdpglem32  38887  addlimc  42113
  Copyright terms: Public domain W3C validator