Theorem simp11r 1286

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

Assertion

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

Proof of Theorem simp11r

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  pceu  16793  maduf  22504  nllyrest  23349  exatleN  39371  2llnjaN  39533  2lplnja  39586  dalemceb  39605  pclfinN  39867  lhpexle3lem  39978  lhpmcvr5N  39994  lhpmcvr6N  39995  lhp2at0  39999  4atexlemw  40015  cdlemd2  40166  cdlemd4  40168  cdleme7aa  40209  cdleme7c  40212  cdleme7d  40213  cdleme7e  40214  cdleme7ga  40215  cdleme7  40216  cdleme15a  40241  cdleme15b  40242  cdleme15d  40244  cdleme15  40245  cdleme16b  40246  cdleme16c  40247  cdleme16d  40248  cdleme16e  40249  cdleme16f  40250  cdleme18d  40262  cdleme19b  40271  cdleme19d  40273  cdleme19e  40274  cdleme20d  40279  cdleme20e  40280  cdleme20f  40281  cdleme20g  40282  cdleme20h  40283  cdleme20j  40285  cdleme20k  40286  cdleme20l1  40287  cdleme20l2  40288  cdleme20l  40289  cdleme20m  40290  cdleme21c  40294  cdleme21ct  40296  cdleme22cN  40309  cdleme22f  40313  cdleme22g  40315  cdleme23a  40316  cdleme23b  40317  cdleme23c  40318  cdleme25a  40320  cdleme25c  40322  cdleme25dN  40323  cdleme26ee  40327  cdleme26eALTN  40328  cdleme27N  40336  cdleme28a  40337  cdleme28b  40338  cdleme29ex  40341  cdlemefr29exN  40369  cdleme32b  40409  cdleme32c  40410  cdleme32e  40412  cdleme35b  40417  cdleme35c  40418  cdleme35d  40419  cdleme35e  40420  cdleme35f  40421  cdleme42h  40449  cdleme42i  40450  cdleme42k  40451  cdleme48bw  40469  cdlemeg46frv  40492  cdlemeg46vrg  40494  cdlemeg46rgv  40495  cdlemeg46req  40496  cdlemf1  40528  trlord  40536  cdlemg7fvbwN  40574  cdlemg10  40608  cdlemg12e  40614  cdlemg12f  40615  cdlemg19a  40650  cdlemg31c  40666  cdlemg33c0  40669  cdlemg35  40680  tendococl  40739  cdlemh2  40783  cdlemh  40784  cdlemi  40787  cdlemk5  40803  cdlemk7  40815  cdlemk11  40816  cdlemk5u  40828  cdlemkj  40830  cdlemkuv2  40834  cdlemk7u  40837  cdlemk11u  40838  cdlemk26-3  40873  cdlemk11t  40913  cdlemk52  40921  cdlemk53a  40922  dihord1  41185  dihord2a  41186  dihord2b  41187  dihord11b  41189  dihord11c  41191  dihord2pre  41192  dihord2pre2  41193  dihord5apre  41229  dihmeetlem1N  41257  dihglblem2N  41261  dihglblem3N  41262  dihglbcpreN  41267  dihmeetlem3N  41272  dihjatc1  41278  suplesup  45308  limsupre  45612  sge0xaddlem2  46405  itscnhlc0yqe  48721  itscnhlc0xyqsol  48727  itsclquadb  48738  itsclquadeu  48739