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

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

Proof of Theorem simp11l
StepHypRef Expression
1 simp1l 1198 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
213ad2ant1 1134 1 ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  pceu  16723  maduf  22006  lshpsmreu  37617  exatleN  37913  2llnjaN  38075  2lplnja  38128  dalemkehl  38132  dath2  38246  pclfinN  38409  lhp2lt  38510  lhpexle3lem  38520  lhpmcvr5N  38536  lhpmcvr6N  38537  lhp2at0  38541  lhp2atnle  38542  lhp2atne  38543  lhp2at0nle  38544  lhp2at0ne  38545  4atexlemk  38556  4atexlemex6  38583  4atexlem7  38584  cdlemd2  38708  cdlemd4  38710  cdlemd7  38713  cdleme0ex2N  38733  cdleme7aa  38751  cdleme7c  38754  cdleme7d  38755  cdleme7e  38756  cdleme7ga  38757  cdleme7  38758  cdleme11c  38770  cdleme11dN  38771  cdleme11e  38772  cdleme11  38779  cdleme14  38782  cdleme15a  38783  cdleme15b  38784  cdleme15c  38785  cdleme15d  38786  cdleme15  38787  cdleme16b  38788  cdleme16c  38789  cdleme16d  38790  cdleme16e  38791  cdleme16f  38792  cdleme18d  38804  cdleme19b  38813  cdleme19d  38815  cdleme19e  38816  cdleme20d  38821  cdleme20e  38822  cdleme20f  38823  cdleme20g  38824  cdleme20h  38825  cdleme20j  38827  cdleme20k  38828  cdleme20l1  38829  cdleme20l2  38830  cdleme20l  38831  cdleme20m  38832  cdleme21c  38836  cdleme21ct  38838  cdleme21d  38839  cdleme21e  38840  cdleme22cN  38851  cdleme22f  38855  cdleme22f2  38856  cdleme22g  38857  cdleme23a  38858  cdleme23b  38859  cdleme23c  38860  cdleme25a  38862  cdleme25c  38864  cdleme25dN  38865  cdleme26ee  38869  cdleme26eALTN  38870  cdleme27a  38876  cdleme27N  38878  cdleme28a  38879  cdleme28b  38880  cdleme29ex  38883  cdlemefrs29bpre0  38905  cdlemefrs29cpre1  38907  cdlemefr29exN  38911  cdleme32fva  38946  cdleme32b  38951  cdleme32c  38952  cdleme32e  38954  cdleme35a  38957  cdleme35fnpq  38958  cdleme35b  38959  cdleme35c  38960  cdleme35d  38961  cdleme35e  38962  cdleme35f  38963  cdleme36a  38969  cdleme37m  38971  cdleme39a  38974  cdleme42e  38988  cdleme42h  38991  cdleme42i  38992  cdleme42k  38993  cdleme43bN  38999  cdleme43dN  39001  cdleme17d2  39004  cdleme48bw  39011  cdlemeg46c  39022  cdlemeg46nlpq  39026  cdlemeg46ngfr  39027  cdlemeg46frv  39034  cdlemeg46vrg  39036  cdlemeg46rgv  39037  cdlemeg46req  39038  cdlemeg46gfv  39039  cdlemf1  39070  trlord  39078  cdlemb3  39115  cdlemg7fvbwN  39116  cdlemg10a  39149  cdlemg10  39150  cdlemg12e  39156  cdlemg12f  39157  cdlemg12g  39158  cdlemg12  39159  cdlemg13a  39160  cdlemg13  39161  cdlemg17b  39171  cdlemg17g  39176  cdlemg17h  39177  cdlemg17pq  39181  cdlemg17  39186  cdlemg19a  39192  cdlemg19  39193  cdlemg21  39195  cdlemg27a  39201  cdlemg27b  39205  cdlemg31c  39208  cdlemg33b0  39210  cdlemg33c0  39211  cdlemg33a  39215  cdlemg33c  39217  cdlemg33e  39219  cdlemg35  39222  trlcone  39237  tendococl  39281  cdlemh1  39324  cdlemh2  39325  cdlemh  39326  cdlemi  39329  cdlemk5  39345  cdlemk6  39346  cdlemki  39350  cdlemksv2  39356  cdlemk7  39357  cdlemk11  39358  cdlemk12  39359  cdlemkole  39362  cdlemk14  39363  cdlemk15  39364  cdlemk17  39367  cdlemk1u  39368  cdlemk5u  39370  cdlemk6u  39371  cdlemkj  39372  cdlemkuv2  39376  cdlemk7u  39379  cdlemk11u  39380  cdlemk12u  39381  cdlemk26-3  39415  cdlemk37  39423  cdlemk11t  39455  cdlemk47  39458  cdlemk48  39459  cdlemk50  39461  cdlemk51  39462  cdlemk52  39463  cdlemk53a  39464  cdlemk39u  39477  dihord1  39727  dihord2a  39728  dihord2b  39729  dihord11b  39731  dihord11c  39733  dihord2pre  39734  dihord2pre2  39735  dihord5apre  39771  dihmeetlem1N  39799  dihglblem2N  39803  dihglblem3N  39804  dihglbcpreN  39809  dihmeetlem3N  39814  dihjatc1  39820  dihjatc2N  39821  dihjatc3  39822  dihmeetlem15N  39830  infleinf  43693  mullimc  43943  mullimcf  43950  limsupre  43968  addlimc  43975  limclner  43978  sge0xaddlem2  44761  itscnhlc0xyqsol  46937  itsclquadb  46948  itsclquadeu  46949
  Copyright terms: Public domain W3C validator