Theorem simp11r 1377

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

Assertion

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

Proof of Theorem simp11r

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  pceu  15764  maduf  20655  nllyrest  21500  exatleN  35182  2llnjaN  35344  2lplnja  35397  dalemceb  35416  pclfinN  35678  lhpexle3lem  35789  lhpmcvr5N  35805  lhpmcvr6N  35806  lhp2at0  35810  4atexlemw  35826  cdlemd2  35977  cdlemd4  35979  cdleme7aa  36020  cdleme7c  36023  cdleme7d  36024  cdleme7e  36025  cdleme7ga  36026  cdleme7  36027  cdleme15a  36052  cdleme15b  36053  cdleme15d  36055  cdleme15  36056  cdleme16b  36057  cdleme16c  36058  cdleme16d  36059  cdleme16e  36060  cdleme16f  36061  cdleme18d  36073  cdleme19b  36082  cdleme19d  36084  cdleme19e  36085  cdleme20d  36090  cdleme20e  36091  cdleme20f  36092  cdleme20g  36093  cdleme20h  36094  cdleme20j  36096  cdleme20k  36097  cdleme20l1  36098  cdleme20l2  36099  cdleme20l  36100  cdleme20m  36101  cdleme21c  36105  cdleme21ct  36107  cdleme22cN  36120  cdleme22f  36124  cdleme22g  36126  cdleme23a  36127  cdleme23b  36128  cdleme23c  36129  cdleme25a  36131  cdleme25c  36133  cdleme25dN  36134  cdleme26ee  36138  cdleme26eALTN  36139  cdleme27N  36147  cdleme28a  36148  cdleme28b  36149  cdleme29ex  36152  cdlemefr29exN  36180  cdleme32b  36220  cdleme32c  36221  cdleme32e  36223  cdleme35b  36228  cdleme35c  36229  cdleme35d  36230  cdleme35e  36231  cdleme35f  36232  cdleme42h  36260  cdleme42i  36261  cdleme42k  36262  cdleme48bw  36280  cdlemeg46frv  36303  cdlemeg46vrg  36305  cdlemeg46rgv  36306  cdlemeg46req  36307  cdlemf1  36339  trlord  36347  cdlemg7fvbwN  36385  cdlemg10  36419  cdlemg12e  36425  cdlemg12f  36426  cdlemg19a  36461  cdlemg31c  36477  cdlemg33c0  36480  cdlemg35  36491  tendococl  36550  cdlemh2  36594  cdlemh  36595  cdlemi  36598  cdlemk5  36614  cdlemk7  36626  cdlemk11  36627  cdlemk5u  36639  cdlemkj  36641  cdlemkuv2  36645  cdlemk7u  36648  cdlemk11u  36649  cdlemk26-3  36684  cdlemk11t  36724  cdlemk52  36732  cdlemk53a  36733  dihord1  36996  dihord2a  36997  dihord2b  36998  dihord11b  37000  dihord11c  37002  dihord2pre  37003  dihord2pre2  37004  dihord5apre  37040  dihmeetlem1N  37068  dihglblem2N  37072  dihglblem3N  37073  dihglbcpreN  37078  dihmeetlem3N  37083  dihjatc1  37089  suplesup  40032  limsupre  40350  sge0xaddlem2  41127