Theorem simp11r 1282

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

Assertion

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

Proof of Theorem simp11r

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

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

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 1086

This theorem is referenced by:  pceu  16834  maduf  22604  nllyrest  23451  exatleN  39027  2llnjaN  39189  2lplnja  39242  dalemceb  39261  pclfinN  39523  lhpexle3lem  39634  lhpmcvr5N  39650  lhpmcvr6N  39651  lhp2at0  39655  4atexlemw  39671  cdlemd2  39822  cdlemd4  39824  cdleme7aa  39865  cdleme7c  39868  cdleme7d  39869  cdleme7e  39870  cdleme7ga  39871  cdleme7  39872  cdleme15a  39897  cdleme15b  39898  cdleme15d  39900  cdleme15  39901  cdleme16b  39902  cdleme16c  39903  cdleme16d  39904  cdleme16e  39905  cdleme16f  39906  cdleme18d  39918  cdleme19b  39927  cdleme19d  39929  cdleme19e  39930  cdleme20d  39935  cdleme20e  39936  cdleme20f  39937  cdleme20g  39938  cdleme20h  39939  cdleme20j  39941  cdleme20k  39942  cdleme20l1  39943  cdleme20l2  39944  cdleme20l  39945  cdleme20m  39946  cdleme21c  39950  cdleme21ct  39952  cdleme22cN  39965  cdleme22f  39969  cdleme22g  39971  cdleme23a  39972  cdleme23b  39973  cdleme23c  39974  cdleme25a  39976  cdleme25c  39978  cdleme25dN  39979  cdleme26ee  39983  cdleme26eALTN  39984  cdleme27N  39992  cdleme28a  39993  cdleme28b  39994  cdleme29ex  39997  cdlemefr29exN  40025  cdleme32b  40065  cdleme32c  40066  cdleme32e  40068  cdleme35b  40073  cdleme35c  40074  cdleme35d  40075  cdleme35e  40076  cdleme35f  40077  cdleme42h  40105  cdleme42i  40106  cdleme42k  40107  cdleme48bw  40125  cdlemeg46frv  40148  cdlemeg46vrg  40150  cdlemeg46rgv  40151  cdlemeg46req  40152  cdlemf1  40184  trlord  40192  cdlemg7fvbwN  40230  cdlemg10  40264  cdlemg12e  40270  cdlemg12f  40271  cdlemg19a  40306  cdlemg31c  40322  cdlemg33c0  40325  cdlemg35  40336  tendococl  40395  cdlemh2  40439  cdlemh  40440  cdlemi  40443  cdlemk5  40459  cdlemk7  40471  cdlemk11  40472  cdlemk5u  40484  cdlemkj  40486  cdlemkuv2  40490  cdlemk7u  40493  cdlemk11u  40494  cdlemk26-3  40529  cdlemk11t  40569  cdlemk52  40577  cdlemk53a  40578  dihord1  40841  dihord2a  40842  dihord2b  40843  dihord11b  40845  dihord11c  40847  dihord2pre  40848  dihord2pre2  40849  dihord5apre  40885  dihmeetlem1N  40913  dihglblem2N  40917  dihglblem3N  40918  dihglbcpreN  40923  dihmeetlem3N  40928  dihjatc1  40934  suplesup  44864  limsupre  45172  sge0xaddlem2  45965  itscnhlc0yqe  48023  itscnhlc0xyqsol  48029  itsclquadb  48040  itsclquadeu  48041