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

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

Proof of Theorem simp12r
StepHypRef Expression
1 simp2r 1086 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜓)
213ad2ant1 1080 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  ackbij1lem16  9001  lsmcv  19060  nllyrest  21199  axcontlem4  25747  eqlkr  33866  athgt  34222  llncvrlpln2  34323  4atlem11b  34374  2lnat  34550  cdlemblem  34559  pclfinN  34666  lhp2at0nle  34801  4atexlemex6  34840  cdlemd2  34966  cdlemd8  34972  cdleme15a  35041  cdleme16b  35046  cdleme16c  35047  cdleme16d  35048  cdleme20h  35084  cdleme21c  35095  cdleme21ct  35097  cdleme22cN  35110  cdleme23b  35118  cdleme26fALTN  35130  cdleme26f  35131  cdleme26f2ALTN  35132  cdleme26f2  35133  cdleme32le  35215  cdleme35f  35222  cdlemf1  35329  trlord  35337  cdlemg7aN  35393  cdlemg33c0  35470  trlcone  35496  cdlemg44  35501  cdlemg48  35505  cdlemky  35694  cdlemk11ta  35697  cdleml4N  35747  dihmeetlem3N  36074  dihmeetlem13N  36088  mapdpglem32  36474  baerlem3lem2  36479  baerlem5alem2  36480  baerlem5blem2  36481  mzpcong  37019
  Copyright terms: Public domain W3C validator