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

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

Proof of Theorem simp11l
StepHypRef Expression
1 simp1l 1240 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
213ad2ant1 1128 1 ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  pceu  15753  maduf  20649  lshpsmreu  34899  exatleN  35193  2llnjaN  35355  2lplnja  35408  dalemkehl  35412  dath2  35526  pclfinN  35689  lhp2lt  35790  lhpexle3lem  35800  lhpmcvr5N  35816  lhpmcvr6N  35817  lhp2at0  35821  lhp2atnle  35822  lhp2atne  35823  lhp2at0nle  35824  lhp2at0ne  35825  4atexlemk  35836  4atexlemex6  35863  4atexlem7  35864  cdlemd2  35989  cdlemd4  35991  cdlemd7  35994  cdleme0ex2N  36014  cdleme7aa  36032  cdleme7c  36035  cdleme7d  36036  cdleme7e  36037  cdleme7ga  36038  cdleme7  36039  cdleme11c  36051  cdleme11dN  36052  cdleme11e  36053  cdleme11  36060  cdleme14  36063  cdleme15a  36064  cdleme15b  36065  cdleme15c  36066  cdleme15d  36067  cdleme15  36068  cdleme16b  36069  cdleme16c  36070  cdleme16d  36071  cdleme16e  36072  cdleme16f  36073  cdleme18d  36085  cdleme19b  36094  cdleme19d  36096  cdleme19e  36097  cdleme20d  36102  cdleme20e  36103  cdleme20f  36104  cdleme20g  36105  cdleme20h  36106  cdleme20j  36108  cdleme20k  36109  cdleme20l1  36110  cdleme20l2  36111  cdleme20l  36112  cdleme20m  36113  cdleme21c  36117  cdleme21ct  36119  cdleme21d  36120  cdleme21e  36121  cdleme22cN  36132  cdleme22f  36136  cdleme22f2  36137  cdleme22g  36138  cdleme23a  36139  cdleme23b  36140  cdleme23c  36141  cdleme25a  36143  cdleme25c  36145  cdleme25dN  36146  cdleme26ee  36150  cdleme26eALTN  36151  cdleme27a  36157  cdleme27N  36159  cdleme28a  36160  cdleme28b  36161  cdleme29ex  36164  cdlemefrs29bpre0  36186  cdlemefrs29cpre1  36188  cdlemefr29exN  36192  cdleme32fva  36227  cdleme32b  36232  cdleme32c  36233  cdleme32e  36235  cdleme35a  36238  cdleme35fnpq  36239  cdleme35b  36240  cdleme35c  36241  cdleme35d  36242  cdleme35e  36243  cdleme35f  36244  cdleme36a  36250  cdleme37m  36252  cdleme39a  36255  cdleme42e  36269  cdleme42h  36272  cdleme42i  36273  cdleme42k  36274  cdleme43bN  36280  cdleme43dN  36282  cdleme17d2  36285  cdleme48bw  36292  cdlemeg46c  36303  cdlemeg46nlpq  36307  cdlemeg46ngfr  36308  cdlemeg46frv  36315  cdlemeg46vrg  36317  cdlemeg46rgv  36318  cdlemeg46req  36319  cdlemeg46gfv  36320  cdlemf1  36351  trlord  36359  cdlemb3  36396  cdlemg7fvbwN  36397  cdlemg10a  36430  cdlemg10  36431  cdlemg12e  36437  cdlemg12f  36438  cdlemg12g  36439  cdlemg12  36440  cdlemg13a  36441  cdlemg13  36442  cdlemg17b  36452  cdlemg17g  36457  cdlemg17h  36458  cdlemg17pq  36462  cdlemg17  36467  cdlemg19a  36473  cdlemg19  36474  cdlemg21  36476  cdlemg27a  36482  cdlemg27b  36486  cdlemg31c  36489  cdlemg33b0  36491  cdlemg33c0  36492  cdlemg33a  36496  cdlemg33c  36498  cdlemg33e  36500  cdlemg35  36503  trlcone  36518  tendococl  36562  cdlemh1  36605  cdlemh2  36606  cdlemh  36607  cdlemi  36610  cdlemk5  36626  cdlemk6  36627  cdlemki  36631  cdlemksv2  36637  cdlemk7  36638  cdlemk11  36639  cdlemk12  36640  cdlemkole  36643  cdlemk14  36644  cdlemk15  36645  cdlemk17  36648  cdlemk1u  36649  cdlemk5u  36651  cdlemk6u  36652  cdlemkj  36653  cdlemkuv2  36657  cdlemk7u  36660  cdlemk11u  36661  cdlemk12u  36662  cdlemk26-3  36696  cdlemk37  36704  cdlemk11t  36736  cdlemk47  36739  cdlemk48  36740  cdlemk50  36742  cdlemk51  36743  cdlemk52  36744  cdlemk53a  36745  cdlemk39u  36758  dihord1  37009  dihord2a  37010  dihord2b  37011  dihord11b  37013  dihord11c  37015  dihord2pre  37016  dihord2pre2  37017  dihord5apre  37053  dihmeetlem1N  37081  dihglblem2N  37085  dihglblem3N  37086  dihglbcpreN  37091  dihmeetlem3N  37096  dihjatc1  37102  dihjatc2N  37103  dihjatc3  37104  dihmeetlem15N  37112  infleinf  40086  mullimc  40351  mullimcf  40358  limsupre  40376  addlimc  40383  limclner  40386  sge0xaddlem2  41154
  Copyright terms: Public domain W3C validator