Theorem simp13l 1287

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

Assertion

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

Proof of Theorem simp13l

Step	Hyp	Ref	Expression
1		simp3l 1200	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant1 1132	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  16879  axpasch  28970  3atlem4  39468  llncvrlpln2  39539  2lplnja  39601  2lnat  39766  llnexchb2  39851  lhp2lt  39983  lhpmcvr5N  40009  4atexlemq  40033  4atexlemex6  40056  trlval2  40145  cdleme7d  40228  cdleme7e  40229  cdleme7ga  40230  cdleme7  40231  cdleme11l  40251  cdleme11  40252  cdleme14  40255  cdleme15a  40256  cdleme15b  40257  cdleme15  40260  cdleme16b  40261  cdleme16c  40262  cdleme16d  40263  cdleme18d  40277  cdleme19b  40286  cdleme19e  40289  cdleme20d  40294  cdleme20g  40297  cdleme20h  40298  cdleme20i  40299  cdleme20j  40300  cdleme20l2  40303  cdleme20l  40304  cdleme20m  40305  cdleme21d  40312  cdleme21e  40313  cdleme21h  40316  cdleme22f  40328  cdleme23a  40331  cdleme23b  40332  cdleme23c  40333  cdleme24  40334  cdleme25a  40335  cdleme25dN  40338  cdleme26ee  40342  cdleme26fALTN  40344  cdleme26f  40345  cdleme26f2ALTN  40346  cdleme26f2  40347  cdleme27a  40349  cdlemefr29bpre0N  40388  cdlemefr29clN  40389  cdlemefr32fvaN  40391  cdlemefr32fva1  40392  cdleme41sn3a  40415  cdleme35a  40430  cdleme35fnpq  40431  cdleme35b  40432  cdleme35c  40433  cdleme35d  40434  cdleme35f  40436  cdleme36m  40443  cdleme37m  40444  cdleme39n  40448  cdleme43bN  40472  cdleme43dN  40474  cdleme17d2  40477  cdlemeg46c  40495  cdlemeg46nlpq  40499  cdlemeg46ngfr  40500  cdlemeg46req  40511  cdlemeg46gfv  40512  cdleme50trn1  40531  cdleme50trn2a  40532  cdlemf1  40543  cdlemf  40545  cdlemg10a  40622  cdlemg10  40623  cdlemg12d  40628  cdlemg12e  40629  cdlemg12f  40630  cdlemg12g  40631  cdlemg12  40632  cdlemg13  40634  cdlemg16ALTN  40640  cdlemg17b  40644  cdlemg17h  40650  cdlemg17pq  40654  cdlemg17iqN  40656  cdlemg17  40659  cdlemg19a  40665  cdlemg19  40666  cdlemg21  40668  cdlemg27a  40674  cdlemg27b  40678  cdlemg31c  40681  cdlemg33b0  40683  cdlemg33a  40688  cdlemg48  40719  tendocan  40806  cdlemk26-3  40888  cdlemk27-3  40889  cdlemk28-3  40890  cdlemk37  40896  cdlemky  40908  cdlemkyu  40909  cdlemk11ta  40911  cdlemkid3N  40915  cdlemk42  40923  cdlemk42yN  40926  cdlemk11t  40928  cdlemk45  40929  cdlemk46  40930  cdlemk47  40931  cdlemk51  40935  cdlemk52  40936  cdlemk53a  40937  cdleml4N  40961  dihord2pre2  41208  dihord4  41240  dihord5apre  41244  dihmeetlem1N  41272  dihmeetlem15N  41303  mapdpglem32  41687  mzpcong  42960  mullimc  45571  mullimcf  45578  addlimc  45603  iscnrm3rlem8  48743