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

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

Proof of Theorem simp11l
StepHypRef Expression
1 simp1l 1083 . 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  15475  maduf  20366  lshpsmreu  33876  exatleN  34170  2llnjaN  34332  2lplnja  34385  dalemkehl  34389  dath2  34503  pclfinN  34666  lhp2lt  34767  lhpexle3lem  34777  lhpmcvr5N  34793  lhpmcvr6N  34794  lhp2at0  34798  lhp2atnle  34799  lhp2atne  34800  lhp2at0nle  34801  lhp2at0ne  34802  4atexlemk  34813  4atexlemex6  34840  4atexlem7  34841  cdlemd2  34966  cdlemd4  34968  cdlemd7  34971  cdleme0ex2N  34991  cdleme7aa  35009  cdleme7c  35012  cdleme7d  35013  cdleme7e  35014  cdleme7ga  35015  cdleme7  35016  cdleme11c  35028  cdleme11dN  35029  cdleme11e  35030  cdleme11  35037  cdleme14  35040  cdleme15a  35041  cdleme15b  35042  cdleme15c  35043  cdleme15d  35044  cdleme15  35045  cdleme16b  35046  cdleme16c  35047  cdleme16d  35048  cdleme16e  35049  cdleme16f  35050  cdleme18d  35062  cdleme19b  35072  cdleme19d  35074  cdleme19e  35075  cdleme20d  35080  cdleme20e  35081  cdleme20f  35082  cdleme20g  35083  cdleme20h  35084  cdleme20j  35086  cdleme20k  35087  cdleme20l1  35088  cdleme20l2  35089  cdleme20l  35090  cdleme20m  35091  cdleme21c  35095  cdleme21ct  35097  cdleme21d  35098  cdleme21e  35099  cdleme22cN  35110  cdleme22f  35114  cdleme22f2  35115  cdleme22g  35116  cdleme23a  35117  cdleme23b  35118  cdleme23c  35119  cdleme25a  35121  cdleme25c  35123  cdleme25dN  35124  cdleme26ee  35128  cdleme26eALTN  35129  cdleme27a  35135  cdleme27N  35137  cdleme28a  35138  cdleme28b  35139  cdleme29ex  35142  cdlemefrs29bpre0  35164  cdlemefrs29cpre1  35166  cdlemefr29exN  35170  cdleme32fva  35205  cdleme32b  35210  cdleme32c  35211  cdleme32e  35213  cdleme35a  35216  cdleme35fnpq  35217  cdleme35b  35218  cdleme35c  35219  cdleme35d  35220  cdleme35e  35221  cdleme35f  35222  cdleme36a  35228  cdleme37m  35230  cdleme39a  35233  cdleme42e  35247  cdleme42h  35250  cdleme42i  35251  cdleme42k  35252  cdleme43bN  35258  cdleme43dN  35260  cdleme17d2  35263  cdleme48bw  35270  cdlemeg46c  35281  cdlemeg46nlpq  35285  cdlemeg46ngfr  35286  cdlemeg46frv  35293  cdlemeg46vrg  35295  cdlemeg46rgv  35296  cdlemeg46req  35297  cdlemeg46gfv  35298  cdlemf1  35329  trlord  35337  cdlemb3  35374  cdlemg7fvbwN  35375  cdlemg10a  35408  cdlemg10  35409  cdlemg12e  35415  cdlemg12f  35416  cdlemg12g  35417  cdlemg12  35418  cdlemg13a  35419  cdlemg13  35420  cdlemg17b  35430  cdlemg17g  35435  cdlemg17h  35436  cdlemg17pq  35440  cdlemg17  35445  cdlemg19a  35451  cdlemg19  35452  cdlemg21  35454  cdlemg27a  35460  cdlemg27b  35464  cdlemg31c  35467  cdlemg33b0  35469  cdlemg33c0  35470  cdlemg33a  35474  cdlemg33c  35476  cdlemg33e  35478  cdlemg35  35481  trlcone  35496  tendococl  35540  cdlemh1  35583  cdlemh2  35584  cdlemh  35585  cdlemi  35588  cdlemk5  35604  cdlemk6  35605  cdlemki  35609  cdlemksv2  35615  cdlemk7  35616  cdlemk11  35617  cdlemk12  35618  cdlemkole  35621  cdlemk14  35622  cdlemk15  35623  cdlemk17  35626  cdlemk1u  35627  cdlemk5u  35629  cdlemk6u  35630  cdlemkj  35631  cdlemkuv2  35635  cdlemk7u  35638  cdlemk11u  35639  cdlemk12u  35640  cdlemk26-3  35674  cdlemk37  35682  cdlemk11t  35714  cdlemk47  35717  cdlemk48  35718  cdlemk50  35720  cdlemk51  35721  cdlemk52  35722  cdlemk53a  35723  cdlemk39u  35736  dihord1  35987  dihord2a  35988  dihord2b  35989  dihord11b  35991  dihord11c  35993  dihord2pre  35994  dihord2pre2  35995  dihord5apre  36031  dihmeetlem1N  36059  dihglblem2N  36063  dihglblem3N  36064  dihglbcpreN  36069  dihmeetlem3N  36074  dihjatc1  36080  dihjatc2N  36081  dihjatc3  36082  dihmeetlem15N  36090  infleinf  39052  mullimc  39252  mullimcf  39259  limsupre  39277  addlimc  39284  limclner  39287  sge0xaddlem2  39958
  Copyright terms: Public domain W3C validator