Theorem simp13l 1285

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

Assertion

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

Proof of Theorem simp13l

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  pceu  16173  axpasch  26735  3atlem4  36782  llncvrlpln2  36853  2lplnja  36915  2lnat  37080  llnexchb2  37165  lhp2lt  37297  lhpmcvr5N  37323  4atexlemq  37347  4atexlemex6  37370  trlval2  37459  cdleme7d  37542  cdleme7e  37543  cdleme7ga  37544  cdleme7  37545  cdleme11l  37565  cdleme11  37566  cdleme14  37569  cdleme15a  37570  cdleme15b  37571  cdleme15  37574  cdleme16b  37575  cdleme16c  37576  cdleme16d  37577  cdleme18d  37591  cdleme19b  37600  cdleme19e  37603  cdleme20d  37608  cdleme20g  37611  cdleme20h  37612  cdleme20i  37613  cdleme20j  37614  cdleme20l2  37617  cdleme20l  37618  cdleme20m  37619  cdleme21d  37626  cdleme21e  37627  cdleme21h  37630  cdleme22f  37642  cdleme23a  37645  cdleme23b  37646  cdleme23c  37647  cdleme24  37648  cdleme25a  37649  cdleme25dN  37652  cdleme26ee  37656  cdleme26fALTN  37658  cdleme26f  37659  cdleme26f2ALTN  37660  cdleme26f2  37661  cdleme27a  37663  cdlemefr29bpre0N  37702  cdlemefr29clN  37703  cdlemefr32fvaN  37705  cdlemefr32fva1  37706  cdleme41sn3a  37729  cdleme35a  37744  cdleme35fnpq  37745  cdleme35b  37746  cdleme35c  37747  cdleme35d  37748  cdleme35f  37750  cdleme36m  37757  cdleme37m  37758  cdleme39n  37762  cdleme43bN  37786  cdleme43dN  37788  cdleme17d2  37791  cdlemeg46c  37809  cdlemeg46nlpq  37813  cdlemeg46ngfr  37814  cdlemeg46req  37825  cdlemeg46gfv  37826  cdleme50trn1  37845  cdleme50trn2a  37846  cdlemf1  37857  cdlemf  37859  cdlemg10a  37936  cdlemg10  37937  cdlemg12d  37942  cdlemg12e  37943  cdlemg12f  37944  cdlemg12g  37945  cdlemg12  37946  cdlemg13  37948  cdlemg16ALTN  37954  cdlemg17b  37958  cdlemg17h  37964  cdlemg17pq  37968  cdlemg17iqN  37970  cdlemg17  37973  cdlemg19a  37979  cdlemg19  37980  cdlemg21  37982  cdlemg27a  37988  cdlemg27b  37992  cdlemg31c  37995  cdlemg33b0  37997  cdlemg33a  38002  cdlemg48  38033  tendocan  38120  cdlemk26-3  38202  cdlemk27-3  38203  cdlemk28-3  38204  cdlemk37  38210  cdlemky  38222  cdlemkyu  38223  cdlemk11ta  38225  cdlemkid3N  38229  cdlemk42  38237  cdlemk42yN  38240  cdlemk11t  38242  cdlemk45  38243  cdlemk46  38244  cdlemk47  38245  cdlemk51  38249  cdlemk52  38250  cdlemk53a  38251  cdleml4N  38275  dihord2pre2  38522  dihord4  38554  dihord5apre  38558  dihmeetlem1N  38586  dihmeetlem15N  38617  mapdpglem32  39001  mzpcong  39913  mullimc  42258  mullimcf  42265  addlimc  42290