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 400   ∧ 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 210  df-an 401  df-3an 1087

This theorem is referenced by:  pceu  16231  axpasch  26827  3atlem4  37055  llncvrlpln2  37126  2lplnja  37188  2lnat  37353  llnexchb2  37438  lhp2lt  37570  lhpmcvr5N  37596  4atexlemq  37620  4atexlemex6  37643  trlval2  37732  cdleme7d  37815  cdleme7e  37816  cdleme7ga  37817  cdleme7  37818  cdleme11l  37838  cdleme11  37839  cdleme14  37842  cdleme15a  37843  cdleme15b  37844  cdleme15  37847  cdleme16b  37848  cdleme16c  37849  cdleme16d  37850  cdleme18d  37864  cdleme19b  37873  cdleme19e  37876  cdleme20d  37881  cdleme20g  37884  cdleme20h  37885  cdleme20i  37886  cdleme20j  37887  cdleme20l2  37890  cdleme20l  37891  cdleme20m  37892  cdleme21d  37899  cdleme21e  37900  cdleme21h  37903  cdleme22f  37915  cdleme23a  37918  cdleme23b  37919  cdleme23c  37920  cdleme24  37921  cdleme25a  37922  cdleme25dN  37925  cdleme26ee  37929  cdleme26fALTN  37931  cdleme26f  37932  cdleme26f2ALTN  37933  cdleme26f2  37934  cdleme27a  37936  cdlemefr29bpre0N  37975  cdlemefr29clN  37976  cdlemefr32fvaN  37978  cdlemefr32fva1  37979  cdleme41sn3a  38002  cdleme35a  38017  cdleme35fnpq  38018  cdleme35b  38019  cdleme35c  38020  cdleme35d  38021  cdleme35f  38023  cdleme36m  38030  cdleme37m  38031  cdleme39n  38035  cdleme43bN  38059  cdleme43dN  38061  cdleme17d2  38064  cdlemeg46c  38082  cdlemeg46nlpq  38086  cdlemeg46ngfr  38087  cdlemeg46req  38098  cdlemeg46gfv  38099  cdleme50trn1  38118  cdleme50trn2a  38119  cdlemf1  38130  cdlemf  38132  cdlemg10a  38209  cdlemg10  38210  cdlemg12d  38215  cdlemg12e  38216  cdlemg12f  38217  cdlemg12g  38218  cdlemg12  38219  cdlemg13  38221  cdlemg16ALTN  38227  cdlemg17b  38231  cdlemg17h  38237  cdlemg17pq  38241  cdlemg17iqN  38243  cdlemg17  38246  cdlemg19a  38252  cdlemg19  38253  cdlemg21  38255  cdlemg27a  38261  cdlemg27b  38265  cdlemg31c  38268  cdlemg33b0  38270  cdlemg33a  38275  cdlemg48  38306  tendocan  38393  cdlemk26-3  38475  cdlemk27-3  38476  cdlemk28-3  38477  cdlemk37  38483  cdlemky  38495  cdlemkyu  38496  cdlemk11ta  38498  cdlemkid3N  38502  cdlemk42  38510  cdlemk42yN  38513  cdlemk11t  38515  cdlemk45  38516  cdlemk46  38517  cdlemk47  38518  cdlemk51  38522  cdlemk52  38523  cdlemk53a  38524  cdleml4N  38548  dihord2pre2  38795  dihord4  38827  dihord5apre  38831  dihmeetlem1N  38859  dihmeetlem15N  38890  mapdpglem32  39274  mzpcong  40279  mullimc  42617  mullimcf  42624  addlimc  42649