Theorem simp13l 1286

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp13l	⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Proof of Theorem simp13l

Step	Hyp	Ref	Expression
1		simp3l 1199	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant1 1131	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  pceu  16528  axpasch  27290  3atlem4  37479  llncvrlpln2  37550  2lplnja  37612  2lnat  37777  llnexchb2  37862  lhp2lt  37994  lhpmcvr5N  38020  4atexlemq  38044  4atexlemex6  38067  trlval2  38156  cdleme7d  38239  cdleme7e  38240  cdleme7ga  38241  cdleme7  38242  cdleme11l  38262  cdleme11  38263  cdleme14  38266  cdleme15a  38267  cdleme15b  38268  cdleme15  38271  cdleme16b  38272  cdleme16c  38273  cdleme16d  38274  cdleme18d  38288  cdleme19b  38297  cdleme19e  38300  cdleme20d  38305  cdleme20g  38308  cdleme20h  38309  cdleme20i  38310  cdleme20j  38311  cdleme20l2  38314  cdleme20l  38315  cdleme20m  38316  cdleme21d  38323  cdleme21e  38324  cdleme21h  38327  cdleme22f  38339  cdleme23a  38342  cdleme23b  38343  cdleme23c  38344  cdleme24  38345  cdleme25a  38346  cdleme25dN  38349  cdleme26ee  38353  cdleme26fALTN  38355  cdleme26f  38356  cdleme26f2ALTN  38357  cdleme26f2  38358  cdleme27a  38360  cdlemefr29bpre0N  38399  cdlemefr29clN  38400  cdlemefr32fvaN  38402  cdlemefr32fva1  38403  cdleme41sn3a  38426  cdleme35a  38441  cdleme35fnpq  38442  cdleme35b  38443  cdleme35c  38444  cdleme35d  38445  cdleme35f  38447  cdleme36m  38454  cdleme37m  38455  cdleme39n  38459  cdleme43bN  38483  cdleme43dN  38485  cdleme17d2  38488  cdlemeg46c  38506  cdlemeg46nlpq  38510  cdlemeg46ngfr  38511  cdlemeg46req  38522  cdlemeg46gfv  38523  cdleme50trn1  38542  cdleme50trn2a  38543  cdlemf1  38554  cdlemf  38556  cdlemg10a  38633  cdlemg10  38634  cdlemg12d  38639  cdlemg12e  38640  cdlemg12f  38641  cdlemg12g  38642  cdlemg12  38643  cdlemg13  38645  cdlemg16ALTN  38651  cdlemg17b  38655  cdlemg17h  38661  cdlemg17pq  38665  cdlemg17iqN  38667  cdlemg17  38670  cdlemg19a  38676  cdlemg19  38677  cdlemg21  38679  cdlemg27a  38685  cdlemg27b  38689  cdlemg31c  38692  cdlemg33b0  38694  cdlemg33a  38699  cdlemg48  38730  tendocan  38817  cdlemk26-3  38899  cdlemk27-3  38900  cdlemk28-3  38901  cdlemk37  38907  cdlemky  38919  cdlemkyu  38920  cdlemk11ta  38922  cdlemkid3N  38926  cdlemk42  38934  cdlemk42yN  38937  cdlemk11t  38939  cdlemk45  38940  cdlemk46  38941  cdlemk47  38942  cdlemk51  38946  cdlemk52  38947  cdlemk53a  38948  cdleml4N  38972  dihord2pre2  39219  dihord4  39251  dihord5apre  39255  dihmeetlem1N  39283  dihmeetlem15N  39314  mapdpglem32  39698  mzpcong  40774  mullimc  43111  mullimcf  43118  addlimc  43143  iscnrm3rlem8  46193