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

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

Proof of Theorem simp13l
StepHypRef Expression
1 simp3l 1087 . 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:  pceu  15486  axpasch  25738  3atlem4  34287  llncvrlpln2  34358  2lplnja  34420  2lnat  34585  llnexchb2  34670  lhp2lt  34802  lhpmcvr5N  34828  4atexlemq  34852  4atexlemex6  34875  trlval2  34965  cdleme7d  35048  cdleme7e  35049  cdleme7ga  35050  cdleme7  35051  cdleme11l  35071  cdleme11  35072  cdleme14  35075  cdleme15a  35076  cdleme15b  35077  cdleme15  35080  cdleme16b  35081  cdleme16c  35082  cdleme16d  35083  cdleme18d  35097  cdleme19b  35107  cdleme19e  35110  cdleme20d  35115  cdleme20g  35118  cdleme20h  35119  cdleme20i  35120  cdleme20j  35121  cdleme20l2  35124  cdleme20l  35125  cdleme20m  35126  cdleme21d  35133  cdleme21e  35134  cdleme21h  35137  cdleme22f  35149  cdleme23a  35152  cdleme23b  35153  cdleme23c  35154  cdleme24  35155  cdleme25a  35156  cdleme25dN  35159  cdleme26ee  35163  cdleme26fALTN  35165  cdleme26f  35166  cdleme26f2ALTN  35167  cdleme26f2  35168  cdleme27a  35170  cdlemefr29bpre0N  35209  cdlemefr29clN  35210  cdlemefr32fvaN  35212  cdlemefr32fva1  35213  cdleme41sn3a  35236  cdleme35a  35251  cdleme35fnpq  35252  cdleme35b  35253  cdleme35c  35254  cdleme35d  35255  cdleme35f  35257  cdleme36m  35264  cdleme37m  35265  cdleme39n  35269  cdleme43bN  35293  cdleme43dN  35295  cdleme17d2  35298  cdlemeg46c  35316  cdlemeg46nlpq  35320  cdlemeg46ngfr  35321  cdlemeg46req  35332  cdlemeg46gfv  35333  cdleme50trn1  35352  cdleme50trn2a  35353  cdlemf1  35364  cdlemf  35366  cdlemg10a  35443  cdlemg10  35444  cdlemg12d  35449  cdlemg12e  35450  cdlemg12f  35451  cdlemg12g  35452  cdlemg12  35453  cdlemg13  35455  cdlemg16ALTN  35461  cdlemg17b  35465  cdlemg17h  35471  cdlemg17pq  35475  cdlemg17iqN  35477  cdlemg17  35480  cdlemg19a  35486  cdlemg19  35487  cdlemg21  35489  cdlemg27a  35495  cdlemg27b  35499  cdlemg31c  35502  cdlemg33b0  35504  cdlemg33a  35509  cdlemg48  35540  tendocan  35627  cdlemk26-3  35709  cdlemk27-3  35710  cdlemk28-3  35711  cdlemk37  35717  cdlemky  35729  cdlemkyu  35730  cdlemk11ta  35732  cdlemkid3N  35736  cdlemk42  35744  cdlemk42yN  35747  cdlemk11t  35749  cdlemk45  35750  cdlemk46  35751  cdlemk47  35752  cdlemk51  35756  cdlemk52  35757  cdlemk53a  35758  cdleml4N  35782  dihord2pre2  36030  dihord4  36062  dihord5apre  36066  dihmeetlem1N  36094  dihmeetlem15N  36125  mapdpglem32  36509  mzpcong  37054  mullimc  39280  mullimcf  39287  addlimc  39312
  Copyright terms: Public domain W3C validator