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

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

Proof of Theorem simp13l
StepHypRef Expression
1 simp3l 1251 . 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:  pceu  15771  axpasch  26041  3atlem4  35268  llncvrlpln2  35339  2lplnja  35401  2lnat  35566  llnexchb2  35651  lhp2lt  35783  lhpmcvr5N  35809  4atexlemq  35833  4atexlemex6  35856  trlval2  35945  cdleme7d  36028  cdleme7e  36029  cdleme7ga  36030  cdleme7  36031  cdleme11l  36051  cdleme11  36052  cdleme14  36055  cdleme15a  36056  cdleme15b  36057  cdleme15  36060  cdleme16b  36061  cdleme16c  36062  cdleme16d  36063  cdleme18d  36077  cdleme19b  36086  cdleme19e  36089  cdleme20d  36094  cdleme20g  36097  cdleme20h  36098  cdleme20i  36099  cdleme20j  36100  cdleme20l2  36103  cdleme20l  36104  cdleme20m  36105  cdleme21d  36112  cdleme21e  36113  cdleme21h  36116  cdleme22f  36128  cdleme23a  36131  cdleme23b  36132  cdleme23c  36133  cdleme24  36134  cdleme25a  36135  cdleme25dN  36138  cdleme26ee  36142  cdleme26fALTN  36144  cdleme26f  36145  cdleme26f2ALTN  36146  cdleme26f2  36147  cdleme27a  36149  cdlemefr29bpre0N  36188  cdlemefr29clN  36189  cdlemefr32fvaN  36191  cdlemefr32fva1  36192  cdleme41sn3a  36215  cdleme35a  36230  cdleme35fnpq  36231  cdleme35b  36232  cdleme35c  36233  cdleme35d  36234  cdleme35f  36236  cdleme36m  36243  cdleme37m  36244  cdleme39n  36248  cdleme43bN  36272  cdleme43dN  36274  cdleme17d2  36277  cdlemeg46c  36295  cdlemeg46nlpq  36299  cdlemeg46ngfr  36300  cdlemeg46req  36311  cdlemeg46gfv  36312  cdleme50trn1  36331  cdleme50trn2a  36332  cdlemf1  36343  cdlemf  36345  cdlemg10a  36422  cdlemg10  36423  cdlemg12d  36428  cdlemg12e  36429  cdlemg12f  36430  cdlemg12g  36431  cdlemg12  36432  cdlemg13  36434  cdlemg16ALTN  36440  cdlemg17b  36444  cdlemg17h  36450  cdlemg17pq  36454  cdlemg17iqN  36456  cdlemg17  36459  cdlemg19a  36465  cdlemg19  36466  cdlemg21  36468  cdlemg27a  36474  cdlemg27b  36478  cdlemg31c  36481  cdlemg33b0  36483  cdlemg33a  36488  cdlemg48  36519  tendocan  36606  cdlemk26-3  36688  cdlemk27-3  36689  cdlemk28-3  36690  cdlemk37  36696  cdlemky  36708  cdlemkyu  36709  cdlemk11ta  36711  cdlemkid3N  36715  cdlemk42  36723  cdlemk42yN  36726  cdlemk11t  36728  cdlemk45  36729  cdlemk46  36730  cdlemk47  36731  cdlemk51  36735  cdlemk52  36736  cdlemk53a  36737  cdleml4N  36761  dihord2pre2  37008  dihord4  37040  dihord5apre  37044  dihmeetlem1N  37072  dihmeetlem15N  37103  mapdpglem32  37487  mzpcong  38041  mullimc  40329  mullimcf  40336  addlimc  40361
  Copyright terms: Public domain W3C validator