Theorem simp11r 1304

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

Assertion

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

Proof of Theorem simp11r

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pceu  17017  maduf  22949  nllyrest  23798  exatleN  40441  2llnjaN  40603  2lplnja  40656  dalemceb  40675  pclfinN  40937  lhpexle3lem  41048  lhpmcvr5N  41064  lhpmcvr6N  41065  lhp2at0  41069  4atexlemw  41085  cdlemd2  41236  cdlemd4  41238  cdleme7aa  41279  cdleme7c  41282  cdleme7d  41283  cdleme7e  41284  cdleme7ga  41285  cdleme7  41286  cdleme15a  41311  cdleme15b  41312  cdleme15d  41314  cdleme15  41315  cdleme16b  41316  cdleme16c  41317  cdleme16d  41318  cdleme16e  41319  cdleme16f  41320  cdleme18d  41332  cdleme19b  41341  cdleme19d  41343  cdleme19e  41344  cdleme20d  41349  cdleme20e  41350  cdleme20f  41351  cdleme20g  41352  cdleme20h  41353  cdleme20j  41355  cdleme20k  41356  cdleme20l1  41357  cdleme20l2  41358  cdleme20l  41359  cdleme20m  41360  cdleme21c  41364  cdleme21ct  41366  cdleme22cN  41379  cdleme22f  41383  cdleme22g  41385  cdleme23a  41386  cdleme23b  41387  cdleme23c  41388  cdleme25a  41390  cdleme25c  41392  cdleme25dN  41393  cdleme26ee  41397  cdleme26eALTN  41398  cdleme27N  41406  cdleme28a  41407  cdleme28b  41408  cdleme29ex  41411  cdlemefr29exN  41439  cdleme32b  41479  cdleme32c  41480  cdleme32e  41482  cdleme35b  41487  cdleme35c  41488  cdleme35d  41489  cdleme35e  41490  cdleme35f  41491  cdleme42h  41519  cdleme42i  41520  cdleme42k  41521  cdleme48bw  41539  cdlemeg46frv  41562  cdlemeg46vrg  41564  cdlemeg46rgv  41565  cdlemeg46req  41566  cdlemf1  41598  trlord  41606  cdlemg7fvbwN  41644  cdlemg10  41678  cdlemg12e  41684  cdlemg12f  41685  cdlemg19a  41720  cdlemg31c  41736  cdlemg33c0  41739  cdlemg35  41750  tendococl  41809  cdlemh2  41853  cdlemh  41854  cdlemi  41857  cdlemk5  41873  cdlemk7  41885  cdlemk11  41886  cdlemk5u  41898  cdlemkj  41900  cdlemkuv2  41904  cdlemk7u  41907  cdlemk11u  41908  cdlemk26-3  41943  cdlemk11t  41983  cdlemk52  41991  cdlemk53a  41992  dihord1  42255  dihord2a  42256  dihord2b  42257  dihord11b  42259  dihord11c  42261  dihord2pre  42262  dihord2pre2  42263  dihord5apre  42299  dihmeetlem1N  42327  dihglblem2N  42331  dihglblem3N  42332  dihglbcpreN  42337  dihmeetlem3N  42342  dihjatc1  42348  suplesup  46320  limsupre  46620  sge0xaddlem2  47413  itscnhlc0yqe  49840  itscnhlc0xyqsol  49846  itsclquadb  49857  itsclquadeu  49858