Theorem simp13l 1289

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

Assertion

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

Proof of Theorem simp13l

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

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

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

This theorem is referenced by:  pceu  16755  axpasch  28917  3atlem4  39524  llncvrlpln2  39595  2lplnja  39657  2lnat  39822  llnexchb2  39907  lhp2lt  40039  lhpmcvr5N  40065  4atexlemq  40089  4atexlemex6  40112  trlval2  40201  cdleme7d  40284  cdleme7e  40285  cdleme7ga  40286  cdleme7  40287  cdleme11l  40307  cdleme11  40308  cdleme14  40311  cdleme15a  40312  cdleme15b  40313  cdleme15  40316  cdleme16b  40317  cdleme16c  40318  cdleme16d  40319  cdleme18d  40333  cdleme19b  40342  cdleme19e  40345  cdleme20d  40350  cdleme20g  40353  cdleme20h  40354  cdleme20i  40355  cdleme20j  40356  cdleme20l2  40359  cdleme20l  40360  cdleme20m  40361  cdleme21d  40368  cdleme21e  40369  cdleme21h  40372  cdleme22f  40384  cdleme23a  40387  cdleme23b  40388  cdleme23c  40389  cdleme24  40390  cdleme25a  40391  cdleme25dN  40394  cdleme26ee  40398  cdleme26fALTN  40400  cdleme26f  40401  cdleme26f2ALTN  40402  cdleme26f2  40403  cdleme27a  40405  cdlemefr29bpre0N  40444  cdlemefr29clN  40445  cdlemefr32fvaN  40447  cdlemefr32fva1  40448  cdleme41sn3a  40471  cdleme35a  40486  cdleme35fnpq  40487  cdleme35b  40488  cdleme35c  40489  cdleme35d  40490  cdleme35f  40492  cdleme36m  40499  cdleme37m  40500  cdleme39n  40504  cdleme43bN  40528  cdleme43dN  40530  cdleme17d2  40533  cdlemeg46c  40551  cdlemeg46nlpq  40555  cdlemeg46ngfr  40556  cdlemeg46req  40567  cdlemeg46gfv  40568  cdleme50trn1  40587  cdleme50trn2a  40588  cdlemf1  40599  cdlemf  40601  cdlemg10a  40678  cdlemg10  40679  cdlemg12d  40684  cdlemg12e  40685  cdlemg12f  40686  cdlemg12g  40687  cdlemg12  40688  cdlemg13  40690  cdlemg16ALTN  40696  cdlemg17b  40700  cdlemg17h  40706  cdlemg17pq  40710  cdlemg17iqN  40712  cdlemg17  40715  cdlemg19a  40721  cdlemg19  40722  cdlemg21  40724  cdlemg27a  40730  cdlemg27b  40734  cdlemg31c  40737  cdlemg33b0  40739  cdlemg33a  40744  cdlemg48  40775  tendocan  40862  cdlemk26-3  40944  cdlemk27-3  40945  cdlemk28-3  40946  cdlemk37  40952  cdlemky  40964  cdlemkyu  40965  cdlemk11ta  40967  cdlemkid3N  40971  cdlemk42  40979  cdlemk42yN  40982  cdlemk11t  40984  cdlemk45  40985  cdlemk46  40986  cdlemk47  40987  cdlemk51  40991  cdlemk52  40992  cdlemk53a  40993  cdleml4N  41017  dihord2pre2  41264  dihord4  41296  dihord5apre  41300  dihmeetlem1N  41328  dihmeetlem15N  41359  mapdpglem32  41743  mzpcong  43004  mullimc  45655  mullimcf  45662  addlimc  45685  iscnrm3rlem8  48977