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

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

Proof of Theorem simp12r
StepHypRef Expression
1 simp2r 1263 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜓)
213ad2ant1 1169 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1113
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 199  df-an 387  df-3an 1115
This theorem is referenced by:  ackbij1lem16  9371  lsmcv  19500  nllyrest  21659  axcontlem4  26265  eqlkr  35173  athgt  35530  llncvrlpln2  35631  4atlem11b  35682  2lnat  35858  cdlemblem  35867  pclfinN  35974  lhp2at0nle  36109  4atexlemex6  36148  cdlemd2  36273  cdlemd8  36279  cdleme15a  36348  cdleme16b  36353  cdleme16c  36354  cdleme16d  36355  cdleme20h  36390  cdleme21c  36401  cdleme21ct  36403  cdleme22cN  36416  cdleme23b  36424  cdleme26fALTN  36436  cdleme26f  36437  cdleme26f2ALTN  36438  cdleme26f2  36439  cdleme32le  36521  cdleme35f  36528  cdlemf1  36635  trlord  36643  cdlemg7aN  36699  cdlemg33c0  36776  trlcone  36802  cdlemg44  36807  cdlemg48  36811  cdlemky  37000  cdlemk11ta  37003  cdleml4N  37053  dihmeetlem3N  37379  dihmeetlem13N  37393  mapdpglem32  37779  baerlem3lem2  37784  baerlem5alem2  37785  baerlem5blem2  37786  mzpcong  38381
  Copyright terms: Public domain W3C validator