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  17004  axpasch  29501  3atlem4  40511  llncvrlpln2  40582  2lplnja  40644  2lnat  40809  llnexchb2  40894  lhp2lt  41026  lhpmcvr5N  41052  4atexlemq  41076  4atexlemex6  41099  trlval2  41188  cdleme7d  41271  cdleme7e  41272  cdleme7ga  41273  cdleme7  41274  cdleme11l  41294  cdleme11  41295  cdleme14  41298  cdleme15a  41299  cdleme15b  41300  cdleme15  41303  cdleme16b  41304  cdleme16c  41305  cdleme16d  41306  cdleme18d  41320  cdleme19b  41329  cdleme19e  41332  cdleme20d  41337  cdleme20g  41340  cdleme20h  41341  cdleme20i  41342  cdleme20j  41343  cdleme20l2  41346  cdleme20l  41347  cdleme20m  41348  cdleme21d  41355  cdleme21e  41356  cdleme21h  41359  cdleme22f  41371  cdleme23a  41374  cdleme23b  41375  cdleme23c  41376  cdleme24  41377  cdleme25a  41378  cdleme25dN  41381  cdleme26ee  41385  cdleme26fALTN  41387  cdleme26f  41388  cdleme26f2ALTN  41389  cdleme26f2  41390  cdleme27a  41392  cdlemefr29bpre0N  41431  cdlemefr29clN  41432  cdlemefr32fvaN  41434  cdlemefr32fva1  41435  cdleme41sn3a  41458  cdleme35a  41473  cdleme35fnpq  41474  cdleme35b  41475  cdleme35c  41476  cdleme35d  41477  cdleme35f  41479  cdleme36m  41486  cdleme37m  41487  cdleme39n  41491  cdleme43bN  41515  cdleme43dN  41517  cdleme17d2  41520  cdlemeg46c  41538  cdlemeg46nlpq  41542  cdlemeg46ngfr  41543  cdlemeg46req  41554  cdlemeg46gfv  41555  cdleme50trn1  41574  cdleme50trn2a  41575  cdlemf1  41586  cdlemf  41588  cdlemg10a  41665  cdlemg10  41666  cdlemg12d  41671  cdlemg12e  41672  cdlemg12f  41673  cdlemg12g  41674  cdlemg12  41675  cdlemg13  41677  cdlemg16ALTN  41683  cdlemg17b  41687  cdlemg17h  41693  cdlemg17pq  41697  cdlemg17iqN  41699  cdlemg17  41702  cdlemg19a  41708  cdlemg19  41709  cdlemg21  41711  cdlemg27a  41717  cdlemg27b  41721  cdlemg31c  41724  cdlemg33b0  41726  cdlemg33a  41731  cdlemg48  41762  tendocan  41849  cdlemk26-3  41931  cdlemk27-3  41932  cdlemk28-3  41933  cdlemk37  41939  cdlemky  41951  cdlemkyu  41952  cdlemk11ta  41954  cdlemkid3N  41958  cdlemk42  41966  cdlemk42yN  41969  cdlemk11t  41971  cdlemk45  41972  cdlemk46  41973  cdlemk47  41974  cdlemk51  41978  cdlemk52  41979  cdlemk53a  41980  cdleml4N  42004  dihord2pre2  42251  dihord4  42283  dihord5apre  42287  dihmeetlem1N  42315  dihmeetlem15N  42346  mapdpglem32  42730  mzpcong  43932  mullimc  46572  mullimcf  46579  addlimc  46602  iscnrm3rlem8  49999