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

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

Proof of Theorem simp12r
StepHypRef Expression
1 simp2r 1242 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜓)
213ad2ant1 1127 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 197  df-an 383  df-3an 1073
This theorem is referenced by:  ackbij1lem16  9259  lsmcv  19355  nllyrest  21510  axcontlem4  26068  eqlkr  34908  athgt  35264  llncvrlpln2  35365  4atlem11b  35416  2lnat  35592  cdlemblem  35601  pclfinN  35708  lhp2at0nle  35843  4atexlemex6  35882  cdlemd2  36008  cdlemd8  36014  cdleme15a  36083  cdleme16b  36088  cdleme16c  36089  cdleme16d  36090  cdleme20h  36125  cdleme21c  36136  cdleme21ct  36138  cdleme22cN  36151  cdleme23b  36159  cdleme26fALTN  36171  cdleme26f  36172  cdleme26f2ALTN  36173  cdleme26f2  36174  cdleme32le  36256  cdleme35f  36263  cdlemf1  36370  trlord  36378  cdlemg7aN  36434  cdlemg33c0  36511  trlcone  36537  cdlemg44  36542  cdlemg48  36546  cdlemky  36735  cdlemk11ta  36738  cdleml4N  36788  dihmeetlem3N  37115  dihmeetlem13N  37129  mapdpglem32  37515  baerlem3lem2  37520  baerlem5alem2  37521  baerlem5blem2  37522  mzpcong  38065
  Copyright terms: Public domain W3C validator