Theorem simp11r 1283

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

Assertion

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

Proof of Theorem simp11r

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  pceu  16783  maduf  22363  nllyrest  23210  exatleN  38578  2llnjaN  38740  2lplnja  38793  dalemceb  38812  pclfinN  39074  lhpexle3lem  39185  lhpmcvr5N  39201  lhpmcvr6N  39202  lhp2at0  39206  4atexlemw  39222  cdlemd2  39373  cdlemd4  39375  cdleme7aa  39416  cdleme7c  39419  cdleme7d  39420  cdleme7e  39421  cdleme7ga  39422  cdleme7  39423  cdleme15a  39448  cdleme15b  39449  cdleme15d  39451  cdleme15  39452  cdleme16b  39453  cdleme16c  39454  cdleme16d  39455  cdleme16e  39456  cdleme16f  39457  cdleme18d  39469  cdleme19b  39478  cdleme19d  39480  cdleme19e  39481  cdleme20d  39486  cdleme20e  39487  cdleme20f  39488  cdleme20g  39489  cdleme20h  39490  cdleme20j  39492  cdleme20k  39493  cdleme20l1  39494  cdleme20l2  39495  cdleme20l  39496  cdleme20m  39497  cdleme21c  39501  cdleme21ct  39503  cdleme22cN  39516  cdleme22f  39520  cdleme22g  39522  cdleme23a  39523  cdleme23b  39524  cdleme23c  39525  cdleme25a  39527  cdleme25c  39529  cdleme25dN  39530  cdleme26ee  39534  cdleme26eALTN  39535  cdleme27N  39543  cdleme28a  39544  cdleme28b  39545  cdleme29ex  39548  cdlemefr29exN  39576  cdleme32b  39616  cdleme32c  39617  cdleme32e  39619  cdleme35b  39624  cdleme35c  39625  cdleme35d  39626  cdleme35e  39627  cdleme35f  39628  cdleme42h  39656  cdleme42i  39657  cdleme42k  39658  cdleme48bw  39676  cdlemeg46frv  39699  cdlemeg46vrg  39701  cdlemeg46rgv  39702  cdlemeg46req  39703  cdlemf1  39735  trlord  39743  cdlemg7fvbwN  39781  cdlemg10  39815  cdlemg12e  39821  cdlemg12f  39822  cdlemg19a  39857  cdlemg31c  39873  cdlemg33c0  39876  cdlemg35  39887  tendococl  39946  cdlemh2  39990  cdlemh  39991  cdlemi  39994  cdlemk5  40010  cdlemk7  40022  cdlemk11  40023  cdlemk5u  40035  cdlemkj  40037  cdlemkuv2  40041  cdlemk7u  40044  cdlemk11u  40045  cdlemk26-3  40080  cdlemk11t  40120  cdlemk52  40128  cdlemk53a  40129  dihord1  40392  dihord2a  40393  dihord2b  40394  dihord11b  40396  dihord11c  40398  dihord2pre  40399  dihord2pre2  40400  dihord5apre  40436  dihmeetlem1N  40464  dihglblem2N  40468  dihglblem3N  40469  dihglbcpreN  40474  dihmeetlem3N  40479  dihjatc1  40485  suplesup  44347  limsupre  44655  sge0xaddlem2  45448  itscnhlc0yqe  47532  itscnhlc0xyqsol  47538  itsclquadb  47549  itsclquadeu  47550