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

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

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 1088

This theorem is referenced by:  pceu  16745  axpasch  28873  3atlem4  39482  llncvrlpln2  39553  2lplnja  39615  2lnat  39780  llnexchb2  39865  lhp2lt  39997  lhpmcvr5N  40023  4atexlemq  40047  4atexlemex6  40070  trlval2  40159  cdleme7d  40242  cdleme7e  40243  cdleme7ga  40244  cdleme7  40245  cdleme11l  40265  cdleme11  40266  cdleme14  40269  cdleme15a  40270  cdleme15b  40271  cdleme15  40274  cdleme16b  40275  cdleme16c  40276  cdleme16d  40277  cdleme18d  40291  cdleme19b  40300  cdleme19e  40303  cdleme20d  40308  cdleme20g  40311  cdleme20h  40312  cdleme20i  40313  cdleme20j  40314  cdleme20l2  40317  cdleme20l  40318  cdleme20m  40319  cdleme21d  40326  cdleme21e  40327  cdleme21h  40330  cdleme22f  40342  cdleme23a  40345  cdleme23b  40346  cdleme23c  40347  cdleme24  40348  cdleme25a  40349  cdleme25dN  40352  cdleme26ee  40356  cdleme26fALTN  40358  cdleme26f  40359  cdleme26f2ALTN  40360  cdleme26f2  40361  cdleme27a  40363  cdlemefr29bpre0N  40402  cdlemefr29clN  40403  cdlemefr32fvaN  40405  cdlemefr32fva1  40406  cdleme41sn3a  40429  cdleme35a  40444  cdleme35fnpq  40445  cdleme35b  40446  cdleme35c  40447  cdleme35d  40448  cdleme35f  40450  cdleme36m  40457  cdleme37m  40458  cdleme39n  40462  cdleme43bN  40486  cdleme43dN  40488  cdleme17d2  40491  cdlemeg46c  40509  cdlemeg46nlpq  40513  cdlemeg46ngfr  40514  cdlemeg46req  40525  cdlemeg46gfv  40526  cdleme50trn1  40545  cdleme50trn2a  40546  cdlemf1  40557  cdlemf  40559  cdlemg10a  40636  cdlemg10  40637  cdlemg12d  40642  cdlemg12e  40643  cdlemg12f  40644  cdlemg12g  40645  cdlemg12  40646  cdlemg13  40648  cdlemg16ALTN  40654  cdlemg17b  40658  cdlemg17h  40664  cdlemg17pq  40668  cdlemg17iqN  40670  cdlemg17  40673  cdlemg19a  40679  cdlemg19  40680  cdlemg21  40682  cdlemg27a  40688  cdlemg27b  40692  cdlemg31c  40695  cdlemg33b0  40697  cdlemg33a  40702  cdlemg48  40733  tendocan  40820  cdlemk26-3  40902  cdlemk27-3  40903  cdlemk28-3  40904  cdlemk37  40910  cdlemky  40922  cdlemkyu  40923  cdlemk11ta  40925  cdlemkid3N  40929  cdlemk42  40937  cdlemk42yN  40940  cdlemk11t  40942  cdlemk45  40943  cdlemk46  40944  cdlemk47  40945  cdlemk51  40949  cdlemk52  40950  cdlemk53a  40951  cdleml4N  40975  dihord2pre2  41222  dihord4  41254  dihord5apre  41258  dihmeetlem1N  41286  dihmeetlem15N  41317  mapdpglem32  41701  mzpcong  42962  mullimc  45613  mullimcf  45620  addlimc  45643  iscnrm3rlem8  48945