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

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

Proof of Theorem simp12r
StepHypRef Expression
1 simp2r 1081 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜓)
213ad2ant1 1075 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  ackbij1lem16  8940  lsmcv  18962  nllyrest  21099  axcontlem4  25647  eqlkr  33404  athgt  33760  llncvrlpln2  33861  4atlem11b  33912  2lnat  34088  cdlemblem  34097  pclfinN  34204  lhp2at0nle  34339  4atexlemex6  34378  cdlemd2  34504  cdlemd8  34510  cdleme15a  34579  cdleme16b  34584  cdleme16c  34585  cdleme16d  34586  cdleme20h  34622  cdleme21c  34633  cdleme21ct  34635  cdleme22cN  34648  cdleme23b  34656  cdleme26fALTN  34668  cdleme26f  34669  cdleme26f2ALTN  34670  cdleme26f2  34671  cdleme32le  34753  cdleme35f  34760  cdlemf1  34867  trlord  34875  cdlemg7aN  34931  cdlemg33c0  35008  trlcone  35034  cdlemg44  35039  cdlemg48  35043  cdlemky  35232  cdlemk11ta  35235  cdleml4N  35285  dihmeetlem3N  35612  dihmeetlem13N  35626  mapdpglem32  36012  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  mzpcong  36557
  Copyright terms: Public domain W3C validator