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  16760  axpasch  28921  3atlem4  39605  llncvrlpln2  39676  2lplnja  39738  2lnat  39903  llnexchb2  39988  lhp2lt  40120  lhpmcvr5N  40146  4atexlemq  40170  4atexlemex6  40193  trlval2  40282  cdleme7d  40365  cdleme7e  40366  cdleme7ga  40367  cdleme7  40368  cdleme11l  40388  cdleme11  40389  cdleme14  40392  cdleme15a  40393  cdleme15b  40394  cdleme15  40397  cdleme16b  40398  cdleme16c  40399  cdleme16d  40400  cdleme18d  40414  cdleme19b  40423  cdleme19e  40426  cdleme20d  40431  cdleme20g  40434  cdleme20h  40435  cdleme20i  40436  cdleme20j  40437  cdleme20l2  40440  cdleme20l  40441  cdleme20m  40442  cdleme21d  40449  cdleme21e  40450  cdleme21h  40453  cdleme22f  40465  cdleme23a  40468  cdleme23b  40469  cdleme23c  40470  cdleme24  40471  cdleme25a  40472  cdleme25dN  40475  cdleme26ee  40479  cdleme26fALTN  40481  cdleme26f  40482  cdleme26f2ALTN  40483  cdleme26f2  40484  cdleme27a  40486  cdlemefr29bpre0N  40525  cdlemefr29clN  40526  cdlemefr32fvaN  40528  cdlemefr32fva1  40529  cdleme41sn3a  40552  cdleme35a  40567  cdleme35fnpq  40568  cdleme35b  40569  cdleme35c  40570  cdleme35d  40571  cdleme35f  40573  cdleme36m  40580  cdleme37m  40581  cdleme39n  40585  cdleme43bN  40609  cdleme43dN  40611  cdleme17d2  40614  cdlemeg46c  40632  cdlemeg46nlpq  40636  cdlemeg46ngfr  40637  cdlemeg46req  40648  cdlemeg46gfv  40649  cdleme50trn1  40668  cdleme50trn2a  40669  cdlemf1  40680  cdlemf  40682  cdlemg10a  40759  cdlemg10  40760  cdlemg12d  40765  cdlemg12e  40766  cdlemg12f  40767  cdlemg12g  40768  cdlemg12  40769  cdlemg13  40771  cdlemg16ALTN  40777  cdlemg17b  40781  cdlemg17h  40787  cdlemg17pq  40791  cdlemg17iqN  40793  cdlemg17  40796  cdlemg19a  40802  cdlemg19  40803  cdlemg21  40805  cdlemg27a  40811  cdlemg27b  40815  cdlemg31c  40818  cdlemg33b0  40820  cdlemg33a  40825  cdlemg48  40856  tendocan  40943  cdlemk26-3  41025  cdlemk27-3  41026  cdlemk28-3  41027  cdlemk37  41033  cdlemky  41045  cdlemkyu  41046  cdlemk11ta  41048  cdlemkid3N  41052  cdlemk42  41060  cdlemk42yN  41063  cdlemk11t  41065  cdlemk45  41066  cdlemk46  41067  cdlemk47  41068  cdlemk51  41072  cdlemk52  41073  cdlemk53a  41074  cdleml4N  41098  dihord2pre2  41345  dihord4  41377  dihord5apre  41381  dihmeetlem1N  41409  dihmeetlem15N  41440  mapdpglem32  41824  mzpcong  43089  mullimc  45740  mullimcf  45747  addlimc  45770  iscnrm3rlem8  49071