Theorem simp11r 1280

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

Assertion

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

Proof of Theorem simp11r

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1082

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 209  df-an 399  df-3an 1084

This theorem is referenced by:  pceu  16175  maduf  21242  nllyrest  22086  exatleN  36532  2llnjaN  36694  2lplnja  36747  dalemceb  36766  pclfinN  37028  lhpexle3lem  37139  lhpmcvr5N  37155  lhpmcvr6N  37156  lhp2at0  37160  4atexlemw  37176  cdlemd2  37327  cdlemd4  37329  cdleme7aa  37370  cdleme7c  37373  cdleme7d  37374  cdleme7e  37375  cdleme7ga  37376  cdleme7  37377  cdleme15a  37402  cdleme15b  37403  cdleme15d  37405  cdleme15  37406  cdleme16b  37407  cdleme16c  37408  cdleme16d  37409  cdleme16e  37410  cdleme16f  37411  cdleme18d  37423  cdleme19b  37432  cdleme19d  37434  cdleme19e  37435  cdleme20d  37440  cdleme20e  37441  cdleme20f  37442  cdleme20g  37443  cdleme20h  37444  cdleme20j  37446  cdleme20k  37447  cdleme20l1  37448  cdleme20l2  37449  cdleme20l  37450  cdleme20m  37451  cdleme21c  37455  cdleme21ct  37457  cdleme22cN  37470  cdleme22f  37474  cdleme22g  37476  cdleme23a  37477  cdleme23b  37478  cdleme23c  37479  cdleme25a  37481  cdleme25c  37483  cdleme25dN  37484  cdleme26ee  37488  cdleme26eALTN  37489  cdleme27N  37497  cdleme28a  37498  cdleme28b  37499  cdleme29ex  37502  cdlemefr29exN  37530  cdleme32b  37570  cdleme32c  37571  cdleme32e  37573  cdleme35b  37578  cdleme35c  37579  cdleme35d  37580  cdleme35e  37581  cdleme35f  37582  cdleme42h  37610  cdleme42i  37611  cdleme42k  37612  cdleme48bw  37630  cdlemeg46frv  37653  cdlemeg46vrg  37655  cdlemeg46rgv  37656  cdlemeg46req  37657  cdlemf1  37689  trlord  37697  cdlemg7fvbwN  37735  cdlemg10  37769  cdlemg12e  37775  cdlemg12f  37776  cdlemg19a  37811  cdlemg31c  37827  cdlemg33c0  37830  cdlemg35  37841  tendococl  37900  cdlemh2  37944  cdlemh  37945  cdlemi  37948  cdlemk5  37964  cdlemk7  37976  cdlemk11  37977  cdlemk5u  37989  cdlemkj  37991  cdlemkuv2  37995  cdlemk7u  37998  cdlemk11u  37999  cdlemk26-3  38034  cdlemk11t  38074  cdlemk52  38082  cdlemk53a  38083  dihord1  38346  dihord2a  38347  dihord2b  38348  dihord11b  38350  dihord11c  38352  dihord2pre  38353  dihord2pre2  38354  dihord5apre  38390  dihmeetlem1N  38418  dihglblem2N  38422  dihglblem3N  38423  dihglbcpreN  38428  dihmeetlem3N  38433  dihjatc1  38439  suplesup  41596  limsupre  41911  sge0xaddlem2  42706  itscnhlc0yqe  44736  itscnhlc0xyqsol  44742  itsclquadb  44753  itsclquadeu  44754