Theorem simp13l 1290

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

Assertion

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

Proof of Theorem simp13l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  pceu  16817  axpasch  29010  3atlem4  39932  llncvrlpln2  40003  2lplnja  40065  2lnat  40230  llnexchb2  40315  lhp2lt  40447  lhpmcvr5N  40473  4atexlemq  40497  4atexlemex6  40520  trlval2  40609  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme11l  40715  cdleme11  40716  cdleme14  40719  cdleme15a  40720  cdleme15b  40721  cdleme15  40724  cdleme16b  40725  cdleme16c  40726  cdleme16d  40727  cdleme18d  40741  cdleme19b  40750  cdleme19e  40753  cdleme20d  40758  cdleme20g  40761  cdleme20h  40762  cdleme20i  40763  cdleme20j  40764  cdleme20l2  40767  cdleme20l  40768  cdleme20m  40769  cdleme21d  40776  cdleme21e  40777  cdleme21h  40780  cdleme22f  40792  cdleme23a  40795  cdleme23b  40796  cdleme23c  40797  cdleme24  40798  cdleme25a  40799  cdleme25dN  40802  cdleme26ee  40806  cdleme26fALTN  40808  cdleme26f  40809  cdleme26f2ALTN  40810  cdleme26f2  40811  cdleme27a  40813  cdlemefr29bpre0N  40852  cdlemefr29clN  40853  cdlemefr32fvaN  40855  cdlemefr32fva1  40856  cdleme41sn3a  40879  cdleme35a  40894  cdleme35fnpq  40895  cdleme35b  40896  cdleme35c  40897  cdleme35d  40898  cdleme35f  40900  cdleme36m  40907  cdleme37m  40908  cdleme39n  40912  cdleme43bN  40936  cdleme43dN  40938  cdleme17d2  40941  cdlemeg46c  40959  cdlemeg46nlpq  40963  cdlemeg46ngfr  40964  cdlemeg46req  40975  cdlemeg46gfv  40976  cdleme50trn1  40995  cdleme50trn2a  40996  cdlemf1  41007  cdlemf  41009  cdlemg10a  41086  cdlemg10  41087  cdlemg12d  41092  cdlemg12e  41093  cdlemg12f  41094  cdlemg12g  41095  cdlemg12  41096  cdlemg13  41098  cdlemg16ALTN  41104  cdlemg17b  41108  cdlemg17h  41114  cdlemg17pq  41118  cdlemg17iqN  41120  cdlemg17  41123  cdlemg19a  41129  cdlemg19  41130  cdlemg21  41132  cdlemg27a  41138  cdlemg27b  41142  cdlemg31c  41145  cdlemg33b0  41147  cdlemg33a  41152  cdlemg48  41183  tendocan  41270  cdlemk26-3  41352  cdlemk27-3  41353  cdlemk28-3  41354  cdlemk37  41360  cdlemky  41372  cdlemkyu  41373  cdlemk11ta  41375  cdlemkid3N  41379  cdlemk42  41387  cdlemk42yN  41390  cdlemk11t  41392  cdlemk45  41393  cdlemk46  41394  cdlemk47  41395  cdlemk51  41399  cdlemk52  41400  cdlemk53a  41401  cdleml4N  41425  dihord2pre2  41672  dihord4  41704  dihord5apre  41708  dihmeetlem1N  41736  dihmeetlem15N  41767  mapdpglem32  42151  mzpcong  43400  mullimc  46046  mullimcf  46053  addlimc  46076  iscnrm3rlem8  49422