Theorem simp13l 1307

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

Assertion

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

Proof of Theorem simp13l

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 1105

This theorem is referenced by:  pceu  16907  axpasch  29269  3atlem4  40238  llncvrlpln2  40309  2lplnja  40371  2lnat  40536  llnexchb2  40621  lhp2lt  40753  lhpmcvr5N  40779  4atexlemq  40803  4atexlemex6  40826  trlval2  40915  cdleme7d  40998  cdleme7e  40999  cdleme7ga  41000  cdleme7  41001  cdleme11l  41021  cdleme11  41022  cdleme14  41025  cdleme15a  41026  cdleme15b  41027  cdleme15  41030  cdleme16b  41031  cdleme16c  41032  cdleme16d  41033  cdleme18d  41047  cdleme19b  41056  cdleme19e  41059  cdleme20d  41064  cdleme20g  41067  cdleme20h  41068  cdleme20i  41069  cdleme20j  41070  cdleme20l2  41073  cdleme20l  41074  cdleme20m  41075  cdleme21d  41082  cdleme21e  41083  cdleme21h  41086  cdleme22f  41098  cdleme23a  41101  cdleme23b  41102  cdleme23c  41103  cdleme24  41104  cdleme25a  41105  cdleme25dN  41108  cdleme26ee  41112  cdleme26fALTN  41114  cdleme26f  41115  cdleme26f2ALTN  41116  cdleme26f2  41117  cdleme27a  41119  cdlemefr29bpre0N  41158  cdlemefr29clN  41159  cdlemefr32fvaN  41161  cdlemefr32fva1  41162  cdleme41sn3a  41185  cdleme35a  41200  cdleme35fnpq  41201  cdleme35b  41202  cdleme35c  41203  cdleme35d  41204  cdleme35f  41206  cdleme36m  41213  cdleme37m  41214  cdleme39n  41218  cdleme43bN  41242  cdleme43dN  41244  cdleme17d2  41247  cdlemeg46c  41265  cdlemeg46nlpq  41269  cdlemeg46ngfr  41270  cdlemeg46req  41281  cdlemeg46gfv  41282  cdleme50trn1  41301  cdleme50trn2a  41302  cdlemf1  41313  cdlemf  41315  cdlemg10a  41392  cdlemg10  41393  cdlemg12d  41398  cdlemg12e  41399  cdlemg12f  41400  cdlemg12g  41401  cdlemg12  41402  cdlemg13  41404  cdlemg16ALTN  41410  cdlemg17b  41414  cdlemg17h  41420  cdlemg17pq  41424  cdlemg17iqN  41426  cdlemg17  41429  cdlemg19a  41435  cdlemg19  41436  cdlemg21  41438  cdlemg27a  41444  cdlemg27b  41448  cdlemg31c  41451  cdlemg33b0  41453  cdlemg33a  41458  cdlemg48  41489  tendocan  41576  cdlemk26-3  41658  cdlemk27-3  41659  cdlemk28-3  41660  cdlemk37  41666  cdlemky  41678  cdlemkyu  41679  cdlemk11ta  41681  cdlemkid3N  41685  cdlemk42  41693  cdlemk42yN  41696  cdlemk11t  41698  cdlemk45  41699  cdlemk46  41700  cdlemk47  41701  cdlemk51  41705  cdlemk52  41706  cdlemk53a  41707  cdleml4N  41731  dihord2pre2  41978  dihord4  42010  dihord5apre  42014  dihmeetlem1N  42042  dihmeetlem15N  42073  mapdpglem32  42457  mzpcong  43679  mullimc  46312  mullimcf  46319  addlimc  46342  iscnrm3rlem8  49702