Theorem simp13l 1288

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

Assertion

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

Proof of Theorem simp13l

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1087

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 398  df-3an 1089

This theorem is referenced by:  pceu  16592  axpasch  27354  3atlem4  37542  llncvrlpln2  37613  2lplnja  37675  2lnat  37840  llnexchb2  37925  lhp2lt  38057  lhpmcvr5N  38083  4atexlemq  38107  4atexlemex6  38130  trlval2  38219  cdleme7d  38302  cdleme7e  38303  cdleme7ga  38304  cdleme7  38305  cdleme11l  38325  cdleme11  38326  cdleme14  38329  cdleme15a  38330  cdleme15b  38331  cdleme15  38334  cdleme16b  38335  cdleme16c  38336  cdleme16d  38337  cdleme18d  38351  cdleme19b  38360  cdleme19e  38363  cdleme20d  38368  cdleme20g  38371  cdleme20h  38372  cdleme20i  38373  cdleme20j  38374  cdleme20l2  38377  cdleme20l  38378  cdleme20m  38379  cdleme21d  38386  cdleme21e  38387  cdleme21h  38390  cdleme22f  38402  cdleme23a  38405  cdleme23b  38406  cdleme23c  38407  cdleme24  38408  cdleme25a  38409  cdleme25dN  38412  cdleme26ee  38416  cdleme26fALTN  38418  cdleme26f  38419  cdleme26f2ALTN  38420  cdleme26f2  38421  cdleme27a  38423  cdlemefr29bpre0N  38462  cdlemefr29clN  38463  cdlemefr32fvaN  38465  cdlemefr32fva1  38466  cdleme41sn3a  38489  cdleme35a  38504  cdleme35fnpq  38505  cdleme35b  38506  cdleme35c  38507  cdleme35d  38508  cdleme35f  38510  cdleme36m  38517  cdleme37m  38518  cdleme39n  38522  cdleme43bN  38546  cdleme43dN  38548  cdleme17d2  38551  cdlemeg46c  38569  cdlemeg46nlpq  38573  cdlemeg46ngfr  38574  cdlemeg46req  38585  cdlemeg46gfv  38586  cdleme50trn1  38605  cdleme50trn2a  38606  cdlemf1  38617  cdlemf  38619  cdlemg10a  38696  cdlemg10  38697  cdlemg12d  38702  cdlemg12e  38703  cdlemg12f  38704  cdlemg12g  38705  cdlemg12  38706  cdlemg13  38708  cdlemg16ALTN  38714  cdlemg17b  38718  cdlemg17h  38724  cdlemg17pq  38728  cdlemg17iqN  38730  cdlemg17  38733  cdlemg19a  38739  cdlemg19  38740  cdlemg21  38742  cdlemg27a  38748  cdlemg27b  38752  cdlemg31c  38755  cdlemg33b0  38757  cdlemg33a  38762  cdlemg48  38793  tendocan  38880  cdlemk26-3  38962  cdlemk27-3  38963  cdlemk28-3  38964  cdlemk37  38970  cdlemky  38982  cdlemkyu  38983  cdlemk11ta  38985  cdlemkid3N  38989  cdlemk42  38997  cdlemk42yN  39000  cdlemk11t  39002  cdlemk45  39003  cdlemk46  39004  cdlemk47  39005  cdlemk51  39009  cdlemk52  39010  cdlemk53a  39011  cdleml4N  39035  dihord2pre2  39282  dihord4  39314  dihord5apre  39318  dihmeetlem1N  39346  dihmeetlem15N  39377  mapdpglem32  39761  mzpcong  40832  mullimc  43206  mullimcf  43213  addlimc  43238  iscnrm3rlem8  46299