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

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

Proof of Theorem simp12l
StepHypRef Expression
1 simp2l 1249 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
213ad2ant1 1156 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  ackbij1lem16  9339  axcontlem4  26057  eqlkr  34876  athgt  35233  llncvrlpln2  35334  4atlem11b  35385  2lnat  35561  cdlemblem  35570  pclfinN  35677  lhp2lt  35778  lhpmcvr5N  35804  lhpmcvr6N  35805  lhp2at0  35809  lhp2atnle  35810  lhp2at0nle  35812  4atexlemex6  35851  cdlemd2  35977  cdlemd7  35982  cdlemd8  35983  cdlemd9  35984  cdleme7aa  36020  cdleme7c  36023  cdleme7d  36024  cdleme7e  36025  cdleme7ga  36026  cdleme7  36027  cdleme11c  36039  cdleme11dN  36040  cdleme11e  36041  cdleme11  36048  cdleme14  36051  cdleme15a  36052  cdleme15b  36053  cdleme15d  36055  cdleme15  36056  cdleme16b  36057  cdleme16c  36058  cdleme16d  36059  cdleme18d  36073  cdleme19b  36082  cdleme19e  36085  cdleme20d  36090  cdleme20g  36093  cdleme20h  36094  cdleme20i  36095  cdleme20j  36096  cdleme20l2  36099  cdleme20l  36100  cdleme20m  36101  cdleme21c  36105  cdleme21ct  36107  cdleme21d  36108  cdleme21e  36109  cdleme22cN  36120  cdleme22f  36124  cdleme22f2  36125  cdleme23a  36127  cdleme23b  36128  cdleme23c  36129  cdleme25a  36131  cdleme25dN  36134  cdleme26fALTN  36140  cdleme26f  36141  cdleme26f2ALTN  36142  cdleme26f2  36143  cdlemefr29bpre0N  36184  cdlemefr29clN  36185  cdlemefr32fvaN  36187  cdlemefr32fva1  36188  cdleme41sn3a  36211  cdleme32le  36225  cdleme35a  36226  cdleme35fnpq  36227  cdleme35b  36228  cdleme35c  36229  cdleme35d  36230  cdleme35e  36231  cdleme35f  36232  cdleme36a  36238  cdleme37m  36240  cdleme39n  36244  cdleme43bN  36268  cdleme43dN  36270  cdleme17d2  36273  cdlemeg46c  36291  cdlemeg46nlpq  36295  cdlemeg46ngfr  36296  cdlemeg46req  36307  cdlemeg46gfv  36308  cdleme50trn1  36327  cdleme50trn2a  36328  cdlemf1  36339  trlord  36347  cdlemb3  36384  cdlemg7fvbwN  36385  cdlemg7aN  36403  cdlemg10a  36418  cdlemg10  36419  cdlemg12d  36424  cdlemg12e  36425  cdlemg12f  36426  cdlemg12g  36427  cdlemg12  36428  cdlemg13a  36429  cdlemg13  36430  cdlemg17b  36440  cdlemg17f  36444  cdlemg17g  36445  cdlemg17h  36446  cdlemg17pq  36450  cdlemg17  36455  cdlemg19a  36461  cdlemg19  36462  cdlemg21  36464  cdlemg27a  36470  cdlemg27b  36474  cdlemg31c  36477  cdlemg33b0  36479  cdlemg33a  36484  trlcone  36506  cdlemg44  36511  cdlemg48  36515  cdlemk37  36692  cdlemky  36704  cdlemk11ta  36707  cdleml4N  36757  dihord1  36996  dihord2pre2  37004  dihord4  37036  dihord5apre  37040  dihmeetlem1N  37068  dihglblem3N  37073  dihglbcpreN  37078  dihmeetlem3N  37083  dihmeetlem13N  37097  mapdpglem32  37483  baerlem3lem2  37488  baerlem5alem2  37489  baerlem5blem2  37490  mzpcong  38037
  Copyright terms: Public domain W3C validator