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  16762  maduf  22559  nllyrest  23404  exatleN  39526  2llnjaN  39688  2lplnja  39741  dalemceb  39760  pclfinN  40022  lhpexle3lem  40133  lhpmcvr5N  40149  lhpmcvr6N  40150  lhp2at0  40154  4atexlemw  40170  cdlemd2  40321  cdlemd4  40323  cdleme7aa  40364  cdleme7c  40367  cdleme7d  40368  cdleme7e  40369  cdleme7ga  40370  cdleme7  40371  cdleme15a  40396  cdleme15b  40397  cdleme15d  40399  cdleme15  40400  cdleme16b  40401  cdleme16c  40402  cdleme16d  40403  cdleme16e  40404  cdleme16f  40405  cdleme18d  40417  cdleme19b  40426  cdleme19d  40428  cdleme19e  40429  cdleme20d  40434  cdleme20e  40435  cdleme20f  40436  cdleme20g  40437  cdleme20h  40438  cdleme20j  40440  cdleme20k  40441  cdleme20l1  40442  cdleme20l2  40443  cdleme20l  40444  cdleme20m  40445  cdleme21c  40449  cdleme21ct  40451  cdleme22cN  40464  cdleme22f  40468  cdleme22g  40470  cdleme23a  40471  cdleme23b  40472  cdleme23c  40473  cdleme25a  40475  cdleme25c  40477  cdleme25dN  40478  cdleme26ee  40482  cdleme26eALTN  40483  cdleme27N  40491  cdleme28a  40492  cdleme28b  40493  cdleme29ex  40496  cdlemefr29exN  40524  cdleme32b  40564  cdleme32c  40565  cdleme32e  40567  cdleme35b  40572  cdleme35c  40573  cdleme35d  40574  cdleme35e  40575  cdleme35f  40576  cdleme42h  40604  cdleme42i  40605  cdleme42k  40606  cdleme48bw  40624  cdlemeg46frv  40647  cdlemeg46vrg  40649  cdlemeg46rgv  40650  cdlemeg46req  40651  cdlemf1  40683  trlord  40691  cdlemg7fvbwN  40729  cdlemg10  40763  cdlemg12e  40769  cdlemg12f  40770  cdlemg19a  40805  cdlemg31c  40821  cdlemg33c0  40824  cdlemg35  40835  tendococl  40894  cdlemh2  40938  cdlemh  40939  cdlemi  40942  cdlemk5  40958  cdlemk7  40970  cdlemk11  40971  cdlemk5u  40983  cdlemkj  40985  cdlemkuv2  40989  cdlemk7u  40992  cdlemk11u  40993  cdlemk26-3  41028  cdlemk11t  41068  cdlemk52  41076  cdlemk53a  41077  dihord1  41340  dihord2a  41341  dihord2b  41342  dihord11b  41344  dihord11c  41346  dihord2pre  41347  dihord2pre2  41348  dihord5apre  41384  dihmeetlem1N  41412  dihglblem2N  41416  dihglblem3N  41417  dihglbcpreN  41422  dihmeetlem3N  41427  dihjatc1  41433  suplesup  45465  limsupre  45766  sge0xaddlem2  46559  itscnhlc0yqe  48887  itscnhlc0xyqsol  48893  itsclquadb  48904  itsclquadeu  48905