Theorem simp11r 1287

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

Assertion

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

Proof of Theorem simp11r

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  pceu  16786  maduf  22597  nllyrest  23442  exatleN  39777  2llnjaN  39939  2lplnja  39992  dalemceb  40011  pclfinN  40273  lhpexle3lem  40384  lhpmcvr5N  40400  lhpmcvr6N  40401  lhp2at0  40405  4atexlemw  40421  cdlemd2  40572  cdlemd4  40574  cdleme7aa  40615  cdleme7c  40618  cdleme7d  40619  cdleme7e  40620  cdleme7ga  40621  cdleme7  40622  cdleme15a  40647  cdleme15b  40648  cdleme15d  40650  cdleme15  40651  cdleme16b  40652  cdleme16c  40653  cdleme16d  40654  cdleme16e  40655  cdleme16f  40656  cdleme18d  40668  cdleme19b  40677  cdleme19d  40679  cdleme19e  40680  cdleme20d  40685  cdleme20e  40686  cdleme20f  40687  cdleme20g  40688  cdleme20h  40689  cdleme20j  40691  cdleme20k  40692  cdleme20l1  40693  cdleme20l2  40694  cdleme20l  40695  cdleme20m  40696  cdleme21c  40700  cdleme21ct  40702  cdleme22cN  40715  cdleme22f  40719  cdleme22g  40721  cdleme23a  40722  cdleme23b  40723  cdleme23c  40724  cdleme25a  40726  cdleme25c  40728  cdleme25dN  40729  cdleme26ee  40733  cdleme26eALTN  40734  cdleme27N  40742  cdleme28a  40743  cdleme28b  40744  cdleme29ex  40747  cdlemefr29exN  40775  cdleme32b  40815  cdleme32c  40816  cdleme32e  40818  cdleme35b  40823  cdleme35c  40824  cdleme35d  40825  cdleme35e  40826  cdleme35f  40827  cdleme42h  40855  cdleme42i  40856  cdleme42k  40857  cdleme48bw  40875  cdlemeg46frv  40898  cdlemeg46vrg  40900  cdlemeg46rgv  40901  cdlemeg46req  40902  cdlemf1  40934  trlord  40942  cdlemg7fvbwN  40980  cdlemg10  41014  cdlemg12e  41020  cdlemg12f  41021  cdlemg19a  41056  cdlemg31c  41072  cdlemg33c0  41075  cdlemg35  41086  tendococl  41145  cdlemh2  41189  cdlemh  41190  cdlemi  41193  cdlemk5  41209  cdlemk7  41221  cdlemk11  41222  cdlemk5u  41234  cdlemkj  41236  cdlemkuv2  41240  cdlemk7u  41243  cdlemk11u  41244  cdlemk26-3  41279  cdlemk11t  41319  cdlemk52  41327  cdlemk53a  41328  dihord1  41591  dihord2a  41592  dihord2b  41593  dihord11b  41595  dihord11c  41597  dihord2pre  41598  dihord2pre2  41599  dihord5apre  41635  dihmeetlem1N  41663  dihglblem2N  41667  dihglblem3N  41668  dihglbcpreN  41673  dihmeetlem3N  41678  dihjatc1  41684  suplesup  45695  limsupre  45996  sge0xaddlem2  46789  itscnhlc0yqe  49116  itscnhlc0xyqsol  49122  itsclquadb  49133  itsclquadeu  49134