Theorem simp11r 1302

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

Assertion

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

Proof of Theorem simp11r

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  pceu  16902  maduf  22763  nllyrest  23608  exatleN  40063  2llnjaN  40225  2lplnja  40278  dalemceb  40297  pclfinN  40559  lhpexle3lem  40670  lhpmcvr5N  40686  lhpmcvr6N  40687  lhp2at0  40691  4atexlemw  40707  cdlemd2  40858  cdlemd4  40860  cdleme7aa  40901  cdleme7c  40904  cdleme7d  40905  cdleme7e  40906  cdleme7ga  40907  cdleme7  40908  cdleme15a  40933  cdleme15b  40934  cdleme15d  40936  cdleme15  40937  cdleme16b  40938  cdleme16c  40939  cdleme16d  40940  cdleme16e  40941  cdleme16f  40942  cdleme18d  40954  cdleme19b  40963  cdleme19d  40965  cdleme19e  40966  cdleme20d  40971  cdleme20e  40972  cdleme20f  40973  cdleme20g  40974  cdleme20h  40975  cdleme20j  40977  cdleme20k  40978  cdleme20l1  40979  cdleme20l2  40980  cdleme20l  40981  cdleme20m  40982  cdleme21c  40986  cdleme21ct  40988  cdleme22cN  41001  cdleme22f  41005  cdleme22g  41007  cdleme23a  41008  cdleme23b  41009  cdleme23c  41010  cdleme25a  41012  cdleme25c  41014  cdleme25dN  41015  cdleme26ee  41019  cdleme26eALTN  41020  cdleme27N  41028  cdleme28a  41029  cdleme28b  41030  cdleme29ex  41033  cdlemefr29exN  41061  cdleme32b  41101  cdleme32c  41102  cdleme32e  41104  cdleme35b  41109  cdleme35c  41110  cdleme35d  41111  cdleme35e  41112  cdleme35f  41113  cdleme42h  41141  cdleme42i  41142  cdleme42k  41143  cdleme48bw  41161  cdlemeg46frv  41184  cdlemeg46vrg  41186  cdlemeg46rgv  41187  cdlemeg46req  41188  cdlemf1  41220  trlord  41228  cdlemg7fvbwN  41266  cdlemg10  41300  cdlemg12e  41306  cdlemg12f  41307  cdlemg19a  41342  cdlemg31c  41358  cdlemg33c0  41361  cdlemg35  41372  tendococl  41431  cdlemh2  41475  cdlemh  41476  cdlemi  41479  cdlemk5  41495  cdlemk7  41507  cdlemk11  41508  cdlemk5u  41520  cdlemkj  41522  cdlemkuv2  41526  cdlemk7u  41529  cdlemk11u  41530  cdlemk26-3  41565  cdlemk11t  41605  cdlemk52  41613  cdlemk53a  41614  dihord1  41877  dihord2a  41878  dihord2b  41879  dihord11b  41881  dihord11c  41883  dihord2pre  41884  dihord2pre2  41885  dihord5apre  41921  dihmeetlem1N  41949  dihglblem2N  41953  dihglblem3N  41954  dihglbcpreN  41959  dihmeetlem3N  41964  dihjatc1  41970  suplesup  45940  limsupre  46240  sge0xaddlem2  47033  itscnhlc0yqe  49417  itscnhlc0xyqsol  49423  itsclquadb  49434  itsclquadeu  49435