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

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

Proof of Theorem simp12r
StepHypRef Expression
1 simp2r 1194 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜓)
213ad2ant1 1127 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1081
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 209  df-an 399  df-3an 1083
This theorem is referenced by:  ackbij1lem16  9649  lsmcv  19905  nllyrest  22086  axcontlem4  26745  eqlkr  36227  athgt  36584  llncvrlpln2  36685  4atlem11b  36736  2lnat  36912  cdlemblem  36921  pclfinN  37028  lhp2at0nle  37163  4atexlemex6  37202  cdlemd2  37327  cdlemd8  37333  cdleme15a  37402  cdleme16b  37407  cdleme16c  37408  cdleme16d  37409  cdleme20h  37444  cdleme21c  37455  cdleme21ct  37457  cdleme22cN  37470  cdleme23b  37478  cdleme26fALTN  37490  cdleme26f  37491  cdleme26f2ALTN  37492  cdleme26f2  37493  cdleme32le  37575  cdleme35f  37582  cdlemf1  37689  trlord  37697  cdlemg7aN  37753  cdlemg33c0  37830  trlcone  37856  cdlemg44  37861  cdlemg48  37865  cdlemky  38054  cdlemk11ta  38057  cdleml4N  38107  dihmeetlem3N  38433  dihmeetlem13N  38447  mapdpglem32  38833  baerlem3lem2  38838  baerlem5alem2  38839  baerlem5blem2  38840  mzpcong  39559
  Copyright terms: Public domain W3C validator