Theorem simp13l 1286

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

Assertion

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

Proof of Theorem simp13l

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

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

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 396  df-3an 1087

This theorem is referenced by:  pceu  16814  axpasch  28751  3atlem4  38959  llncvrlpln2  39030  2lplnja  39092  2lnat  39257  llnexchb2  39342  lhp2lt  39474  lhpmcvr5N  39500  4atexlemq  39524  4atexlemex6  39547  trlval2  39636  cdleme7d  39719  cdleme7e  39720  cdleme7ga  39721  cdleme7  39722  cdleme11l  39742  cdleme11  39743  cdleme14  39746  cdleme15a  39747  cdleme15b  39748  cdleme15  39751  cdleme16b  39752  cdleme16c  39753  cdleme16d  39754  cdleme18d  39768  cdleme19b  39777  cdleme19e  39780  cdleme20d  39785  cdleme20g  39788  cdleme20h  39789  cdleme20i  39790  cdleme20j  39791  cdleme20l2  39794  cdleme20l  39795  cdleme20m  39796  cdleme21d  39803  cdleme21e  39804  cdleme21h  39807  cdleme22f  39819  cdleme23a  39822  cdleme23b  39823  cdleme23c  39824  cdleme24  39825  cdleme25a  39826  cdleme25dN  39829  cdleme26ee  39833  cdleme26fALTN  39835  cdleme26f  39836  cdleme26f2ALTN  39837  cdleme26f2  39838  cdleme27a  39840  cdlemefr29bpre0N  39879  cdlemefr29clN  39880  cdlemefr32fvaN  39882  cdlemefr32fva1  39883  cdleme41sn3a  39906  cdleme35a  39921  cdleme35fnpq  39922  cdleme35b  39923  cdleme35c  39924  cdleme35d  39925  cdleme35f  39927  cdleme36m  39934  cdleme37m  39935  cdleme39n  39939  cdleme43bN  39963  cdleme43dN  39965  cdleme17d2  39968  cdlemeg46c  39986  cdlemeg46nlpq  39990  cdlemeg46ngfr  39991  cdlemeg46req  40002  cdlemeg46gfv  40003  cdleme50trn1  40022  cdleme50trn2a  40023  cdlemf1  40034  cdlemf  40036  cdlemg10a  40113  cdlemg10  40114  cdlemg12d  40119  cdlemg12e  40120  cdlemg12f  40121  cdlemg12g  40122  cdlemg12  40123  cdlemg13  40125  cdlemg16ALTN  40131  cdlemg17b  40135  cdlemg17h  40141  cdlemg17pq  40145  cdlemg17iqN  40147  cdlemg17  40150  cdlemg19a  40156  cdlemg19  40157  cdlemg21  40159  cdlemg27a  40165  cdlemg27b  40169  cdlemg31c  40172  cdlemg33b0  40174  cdlemg33a  40179  cdlemg48  40210  tendocan  40297  cdlemk26-3  40379  cdlemk27-3  40380  cdlemk28-3  40381  cdlemk37  40387  cdlemky  40399  cdlemkyu  40400  cdlemk11ta  40402  cdlemkid3N  40406  cdlemk42  40414  cdlemk42yN  40417  cdlemk11t  40419  cdlemk45  40420  cdlemk46  40421  cdlemk47  40422  cdlemk51  40426  cdlemk52  40427  cdlemk53a  40428  cdleml4N  40452  dihord2pre2  40699  dihord4  40731  dihord5apre  40735  dihmeetlem1N  40763  dihmeetlem15N  40794  mapdpglem32  41178  mzpcong  42393  mullimc  45004  mullimcf  45011  addlimc  45036  iscnrm3rlem8  47966

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »