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 1134	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  pceu  16779  axpasch  28230  3atlem4  38405  llncvrlpln2  38476  2lplnja  38538  2lnat  38703  llnexchb2  38788  lhp2lt  38920  lhpmcvr5N  38946  4atexlemq  38970  4atexlemex6  38993  trlval2  39082  cdleme7d  39165  cdleme7e  39166  cdleme7ga  39167  cdleme7  39168  cdleme11l  39188  cdleme11  39189  cdleme14  39192  cdleme15a  39193  cdleme15b  39194  cdleme15  39197  cdleme16b  39198  cdleme16c  39199  cdleme16d  39200  cdleme18d  39214  cdleme19b  39223  cdleme19e  39226  cdleme20d  39231  cdleme20g  39234  cdleme20h  39235  cdleme20i  39236  cdleme20j  39237  cdleme20l2  39240  cdleme20l  39241  cdleme20m  39242  cdleme21d  39249  cdleme21e  39250  cdleme21h  39253  cdleme22f  39265  cdleme23a  39268  cdleme23b  39269  cdleme23c  39270  cdleme24  39271  cdleme25a  39272  cdleme25dN  39275  cdleme26ee  39279  cdleme26fALTN  39281  cdleme26f  39282  cdleme26f2ALTN  39283  cdleme26f2  39284  cdleme27a  39286  cdlemefr29bpre0N  39325  cdlemefr29clN  39326  cdlemefr32fvaN  39328  cdlemefr32fva1  39329  cdleme41sn3a  39352  cdleme35a  39367  cdleme35fnpq  39368  cdleme35b  39369  cdleme35c  39370  cdleme35d  39371  cdleme35f  39373  cdleme36m  39380  cdleme37m  39381  cdleme39n  39385  cdleme43bN  39409  cdleme43dN  39411  cdleme17d2  39414  cdlemeg46c  39432  cdlemeg46nlpq  39436  cdlemeg46ngfr  39437  cdlemeg46req  39448  cdlemeg46gfv  39449  cdleme50trn1  39468  cdleme50trn2a  39469  cdlemf1  39480  cdlemf  39482  cdlemg10a  39559  cdlemg10  39560  cdlemg12d  39565  cdlemg12e  39566  cdlemg12f  39567  cdlemg12g  39568  cdlemg12  39569  cdlemg13  39571  cdlemg16ALTN  39577  cdlemg17b  39581  cdlemg17h  39587  cdlemg17pq  39591  cdlemg17iqN  39593  cdlemg17  39596  cdlemg19a  39602  cdlemg19  39603  cdlemg21  39605  cdlemg27a  39611  cdlemg27b  39615  cdlemg31c  39618  cdlemg33b0  39620  cdlemg33a  39625  cdlemg48  39656  tendocan  39743  cdlemk26-3  39825  cdlemk27-3  39826  cdlemk28-3  39827  cdlemk37  39833  cdlemky  39845  cdlemkyu  39846  cdlemk11ta  39848  cdlemkid3N  39852  cdlemk42  39860  cdlemk42yN  39863  cdlemk11t  39865  cdlemk45  39866  cdlemk46  39867  cdlemk47  39868  cdlemk51  39872  cdlemk52  39873  cdlemk53a  39874  cdleml4N  39898  dihord2pre2  40145  dihord4  40177  dihord5apre  40181  dihmeetlem1N  40209  dihmeetlem15N  40240  mapdpglem32  40624  mzpcong  41759  mullimc  44380  mullimcf  44387  addlimc  44412  iscnrm3rlem8  47628