Theorem simp11r 1286

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

Assertion

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

Proof of Theorem simp11r

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

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

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 1088

This theorem is referenced by:  pceu  16774  maduf  22585  nllyrest  23430  exatleN  39664  2llnjaN  39826  2lplnja  39879  dalemceb  39898  pclfinN  40160  lhpexle3lem  40271  lhpmcvr5N  40287  lhpmcvr6N  40288  lhp2at0  40292  4atexlemw  40308  cdlemd2  40459  cdlemd4  40461  cdleme7aa  40502  cdleme7c  40505  cdleme7d  40506  cdleme7e  40507  cdleme7ga  40508  cdleme7  40509  cdleme15a  40534  cdleme15b  40535  cdleme15d  40537  cdleme15  40538  cdleme16b  40539  cdleme16c  40540  cdleme16d  40541  cdleme16e  40542  cdleme16f  40543  cdleme18d  40555  cdleme19b  40564  cdleme19d  40566  cdleme19e  40567  cdleme20d  40572  cdleme20e  40573  cdleme20f  40574  cdleme20g  40575  cdleme20h  40576  cdleme20j  40578  cdleme20k  40579  cdleme20l1  40580  cdleme20l2  40581  cdleme20l  40582  cdleme20m  40583  cdleme21c  40587  cdleme21ct  40589  cdleme22cN  40602  cdleme22f  40606  cdleme22g  40608  cdleme23a  40609  cdleme23b  40610  cdleme23c  40611  cdleme25a  40613  cdleme25c  40615  cdleme25dN  40616  cdleme26ee  40620  cdleme26eALTN  40621  cdleme27N  40629  cdleme28a  40630  cdleme28b  40631  cdleme29ex  40634  cdlemefr29exN  40662  cdleme32b  40702  cdleme32c  40703  cdleme32e  40705  cdleme35b  40710  cdleme35c  40711  cdleme35d  40712  cdleme35e  40713  cdleme35f  40714  cdleme42h  40742  cdleme42i  40743  cdleme42k  40744  cdleme48bw  40762  cdlemeg46frv  40785  cdlemeg46vrg  40787  cdlemeg46rgv  40788  cdlemeg46req  40789  cdlemf1  40821  trlord  40829  cdlemg7fvbwN  40867  cdlemg10  40901  cdlemg12e  40907  cdlemg12f  40908  cdlemg19a  40943  cdlemg31c  40959  cdlemg33c0  40962  cdlemg35  40973  tendococl  41032  cdlemh2  41076  cdlemh  41077  cdlemi  41080  cdlemk5  41096  cdlemk7  41108  cdlemk11  41109  cdlemk5u  41121  cdlemkj  41123  cdlemkuv2  41127  cdlemk7u  41130  cdlemk11u  41131  cdlemk26-3  41166  cdlemk11t  41206  cdlemk52  41214  cdlemk53a  41215  dihord1  41478  dihord2a  41479  dihord2b  41480  dihord11b  41482  dihord11c  41484  dihord2pre  41485  dihord2pre2  41486  dihord5apre  41522  dihmeetlem1N  41550  dihglblem2N  41554  dihglblem3N  41555  dihglbcpreN  41560  dihmeetlem3N  41565  dihjatc1  41571  suplesup  45584  limsupre  45885  sge0xaddlem2  46678  itscnhlc0yqe  49005  itscnhlc0xyqsol  49011  itsclquadb  49022  itsclquadeu  49023