Theorem simp13l 1391

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

Assertion

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

Proof of Theorem simp13l

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1111

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 199  df-an 387  df-3an 1113

This theorem is referenced by:  pceu  15929  axpasch  26247  3atlem4  35560  llncvrlpln2  35631  2lplnja  35693  2lnat  35858  llnexchb2  35943  lhp2lt  36075  lhpmcvr5N  36101  4atexlemq  36125  4atexlemex6  36148  trlval2  36237  cdleme7d  36320  cdleme7e  36321  cdleme7ga  36322  cdleme7  36323  cdleme11l  36343  cdleme11  36344  cdleme14  36347  cdleme15a  36348  cdleme15b  36349  cdleme15  36352  cdleme16b  36353  cdleme16c  36354  cdleme16d  36355  cdleme18d  36369  cdleme19b  36378  cdleme19e  36381  cdleme20d  36386  cdleme20g  36389  cdleme20h  36390  cdleme20i  36391  cdleme20j  36392  cdleme20l2  36395  cdleme20l  36396  cdleme20m  36397  cdleme21d  36404  cdleme21e  36405  cdleme21h  36408  cdleme22f  36420  cdleme23a  36423  cdleme23b  36424  cdleme23c  36425  cdleme24  36426  cdleme25a  36427  cdleme25dN  36430  cdleme26ee  36434  cdleme26fALTN  36436  cdleme26f  36437  cdleme26f2ALTN  36438  cdleme26f2  36439  cdleme27a  36441  cdlemefr29bpre0N  36480  cdlemefr29clN  36481  cdlemefr32fvaN  36483  cdlemefr32fva1  36484  cdleme41sn3a  36507  cdleme35a  36522  cdleme35fnpq  36523  cdleme35b  36524  cdleme35c  36525  cdleme35d  36526  cdleme35f  36528  cdleme36m  36535  cdleme37m  36536  cdleme39n  36540  cdleme43bN  36564  cdleme43dN  36566  cdleme17d2  36569  cdlemeg46c  36587  cdlemeg46nlpq  36591  cdlemeg46ngfr  36592  cdlemeg46req  36603  cdlemeg46gfv  36604  cdleme50trn1  36623  cdleme50trn2a  36624  cdlemf1  36635  cdlemf  36637  cdlemg10a  36714  cdlemg10  36715  cdlemg12d  36720  cdlemg12e  36721  cdlemg12f  36722  cdlemg12g  36723  cdlemg12  36724  cdlemg13  36726  cdlemg16ALTN  36732  cdlemg17b  36736  cdlemg17h  36742  cdlemg17pq  36746  cdlemg17iqN  36748  cdlemg17  36751  cdlemg19a  36757  cdlemg19  36758  cdlemg21  36760  cdlemg27a  36766  cdlemg27b  36770  cdlemg31c  36773  cdlemg33b0  36775  cdlemg33a  36780  cdlemg48  36811  tendocan  36898  cdlemk26-3  36980  cdlemk27-3  36981  cdlemk28-3  36982  cdlemk37  36988  cdlemky  37000  cdlemkyu  37001  cdlemk11ta  37003  cdlemkid3N  37007  cdlemk42  37015  cdlemk42yN  37018  cdlemk11t  37020  cdlemk45  37021  cdlemk46  37022  cdlemk47  37023  cdlemk51  37027  cdlemk52  37028  cdlemk53a  37029  cdleml4N  37053  dihord2pre2  37300  dihord4  37332  dihord5apre  37336  dihmeetlem1N  37364  dihmeetlem15N  37395  mapdpglem32  37779  mzpcong  38381  mullimc  40641  mullimcf  40648  addlimc  40673