Theorem simp13l 1307

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

Assertion

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

Proof of Theorem simp13l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pceu  17029  axpasch  29524  3atlem4  40636  llncvrlpln2  40707  2lplnja  40769  2lnat  40934  llnexchb2  41019  lhp2lt  41151  lhpmcvr5N  41177  4atexlemq  41201  4atexlemex6  41224  trlval2  41313  cdleme7d  41396  cdleme7e  41397  cdleme7ga  41398  cdleme7  41399  cdleme11l  41419  cdleme11  41420  cdleme14  41423  cdleme15a  41424  cdleme15b  41425  cdleme15  41428  cdleme16b  41429  cdleme16c  41430  cdleme16d  41431  cdleme18d  41445  cdleme19b  41454  cdleme19e  41457  cdleme20d  41462  cdleme20g  41465  cdleme20h  41466  cdleme20i  41467  cdleme20j  41468  cdleme20l2  41471  cdleme20l  41472  cdleme20m  41473  cdleme21d  41480  cdleme21e  41481  cdleme21h  41484  cdleme22f  41496  cdleme23a  41499  cdleme23b  41500  cdleme23c  41501  cdleme24  41502  cdleme25a  41503  cdleme25dN  41506  cdleme26ee  41510  cdleme26fALTN  41512  cdleme26f  41513  cdleme26f2ALTN  41514  cdleme26f2  41515  cdleme27a  41517  cdlemefr29bpre0N  41556  cdlemefr29clN  41557  cdlemefr32fvaN  41559  cdlemefr32fva1  41560  cdleme41sn3a  41583  cdleme35a  41598  cdleme35fnpq  41599  cdleme35b  41600  cdleme35c  41601  cdleme35d  41602  cdleme35f  41604  cdleme36m  41611  cdleme37m  41612  cdleme39n  41616  cdleme43bN  41640  cdleme43dN  41642  cdleme17d2  41645  cdlemeg46c  41663  cdlemeg46nlpq  41667  cdlemeg46ngfr  41668  cdlemeg46req  41679  cdlemeg46gfv  41680  cdleme50trn1  41699  cdleme50trn2a  41700  cdlemf1  41711  cdlemf  41713  cdlemg10a  41790  cdlemg10  41791  cdlemg12d  41796  cdlemg12e  41797  cdlemg12f  41798  cdlemg12g  41799  cdlemg12  41800  cdlemg13  41802  cdlemg16ALTN  41808  cdlemg17b  41812  cdlemg17h  41818  cdlemg17pq  41822  cdlemg17iqN  41824  cdlemg17  41827  cdlemg19a  41833  cdlemg19  41834  cdlemg21  41836  cdlemg27a  41842  cdlemg27b  41846  cdlemg31c  41849  cdlemg33b0  41851  cdlemg33a  41856  cdlemg48  41887  tendocan  41974  cdlemk26-3  42056  cdlemk27-3  42057  cdlemk28-3  42058  cdlemk37  42064  cdlemky  42076  cdlemkyu  42077  cdlemk11ta  42079  cdlemkid3N  42083  cdlemk42  42091  cdlemk42yN  42094  cdlemk11t  42096  cdlemk45  42097  cdlemk46  42098  cdlemk47  42099  cdlemk51  42103  cdlemk52  42104  cdlemk53a  42105  cdleml4N  42129  dihord2pre2  42376  dihord4  42408  dihord5apre  42412  dihmeetlem1N  42440  dihmeetlem15N  42471  mapdpglem32  42855  mzpcong  44072  mullimc  46721  mullimcf  46728  addlimc  46751  iscnrm3rlem8  50154