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

This theorem is referenced by:  pceu  16575  maduf  21818  nllyrest  22665  exatleN  37444  2llnjaN  37606  2lplnja  37659  dalemceb  37678  pclfinN  37940  lhpexle3lem  38051  lhpmcvr5N  38067  lhpmcvr6N  38068  lhp2at0  38072  4atexlemw  38088  cdlemd2  38239  cdlemd4  38241  cdleme7aa  38282  cdleme7c  38285  cdleme7d  38286  cdleme7e  38287  cdleme7ga  38288  cdleme7  38289  cdleme15a  38314  cdleme15b  38315  cdleme15d  38317  cdleme15  38318  cdleme16b  38319  cdleme16c  38320  cdleme16d  38321  cdleme16e  38322  cdleme16f  38323  cdleme18d  38335  cdleme19b  38344  cdleme19d  38346  cdleme19e  38347  cdleme20d  38352  cdleme20e  38353  cdleme20f  38354  cdleme20g  38355  cdleme20h  38356  cdleme20j  38358  cdleme20k  38359  cdleme20l1  38360  cdleme20l2  38361  cdleme20l  38362  cdleme20m  38363  cdleme21c  38367  cdleme21ct  38369  cdleme22cN  38382  cdleme22f  38386  cdleme22g  38388  cdleme23a  38389  cdleme23b  38390  cdleme23c  38391  cdleme25a  38393  cdleme25c  38395  cdleme25dN  38396  cdleme26ee  38400  cdleme26eALTN  38401  cdleme27N  38409  cdleme28a  38410  cdleme28b  38411  cdleme29ex  38414  cdlemefr29exN  38442  cdleme32b  38482  cdleme32c  38483  cdleme32e  38485  cdleme35b  38490  cdleme35c  38491  cdleme35d  38492  cdleme35e  38493  cdleme35f  38494  cdleme42h  38522  cdleme42i  38523  cdleme42k  38524  cdleme48bw  38542  cdlemeg46frv  38565  cdlemeg46vrg  38567  cdlemeg46rgv  38568  cdlemeg46req  38569  cdlemf1  38601  trlord  38609  cdlemg7fvbwN  38647  cdlemg10  38681  cdlemg12e  38687  cdlemg12f  38688  cdlemg19a  38723  cdlemg31c  38739  cdlemg33c0  38742  cdlemg35  38753  tendococl  38812  cdlemh2  38856  cdlemh  38857  cdlemi  38860  cdlemk5  38876  cdlemk7  38888  cdlemk11  38889  cdlemk5u  38901  cdlemkj  38903  cdlemkuv2  38907  cdlemk7u  38910  cdlemk11u  38911  cdlemk26-3  38946  cdlemk11t  38986  cdlemk52  38994  cdlemk53a  38995  dihord1  39258  dihord2a  39259  dihord2b  39260  dihord11b  39262  dihord11c  39264  dihord2pre  39265  dihord2pre2  39266  dihord5apre  39302  dihmeetlem1N  39330  dihglblem2N  39334  dihglblem3N  39335  dihglbcpreN  39340  dihmeetlem3N  39345  dihjatc1  39351  suplesup  42912  limsupre  43217  sge0xaddlem2  44008  itscnhlc0yqe  46145  itscnhlc0xyqsol  46151  itsclquadb  46162  itsclquadeu  46163