Theorem simp11r 1266

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

Assertion

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

Proof of Theorem simp11r

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1069

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 199  df-an 388  df-3an 1071

This theorem is referenced by:  pceu  16037  maduf  20969  nllyrest  21813  exatleN  36022  2llnjaN  36184  2lplnja  36237  dalemceb  36256  pclfinN  36518  lhpexle3lem  36629  lhpmcvr5N  36645  lhpmcvr6N  36646  lhp2at0  36650  4atexlemw  36666  cdlemd2  36817  cdlemd4  36819  cdleme7aa  36860  cdleme7c  36863  cdleme7d  36864  cdleme7e  36865  cdleme7ga  36866  cdleme7  36867  cdleme15a  36892  cdleme15b  36893  cdleme15d  36895  cdleme15  36896  cdleme16b  36897  cdleme16c  36898  cdleme16d  36899  cdleme16e  36900  cdleme16f  36901  cdleme18d  36913  cdleme19b  36922  cdleme19d  36924  cdleme19e  36925  cdleme20d  36930  cdleme20e  36931  cdleme20f  36932  cdleme20g  36933  cdleme20h  36934  cdleme20j  36936  cdleme20k  36937  cdleme20l1  36938  cdleme20l2  36939  cdleme20l  36940  cdleme20m  36941  cdleme21c  36945  cdleme21ct  36947  cdleme22cN  36960  cdleme22f  36964  cdleme22g  36966  cdleme23a  36967  cdleme23b  36968  cdleme23c  36969  cdleme25a  36971  cdleme25c  36973  cdleme25dN  36974  cdleme26ee  36978  cdleme26eALTN  36979  cdleme27N  36987  cdleme28a  36988  cdleme28b  36989  cdleme29ex  36992  cdlemefr29exN  37020  cdleme32b  37060  cdleme32c  37061  cdleme32e  37063  cdleme35b  37068  cdleme35c  37069  cdleme35d  37070  cdleme35e  37071  cdleme35f  37072  cdleme42h  37100  cdleme42i  37101  cdleme42k  37102  cdleme48bw  37120  cdlemeg46frv  37143  cdlemeg46vrg  37145  cdlemeg46rgv  37146  cdlemeg46req  37147  cdlemf1  37179  trlord  37187  cdlemg7fvbwN  37225  cdlemg10  37259  cdlemg12e  37265  cdlemg12f  37266  cdlemg19a  37301  cdlemg31c  37317  cdlemg33c0  37320  cdlemg35  37331  tendococl  37390  cdlemh2  37434  cdlemh  37435  cdlemi  37438  cdlemk5  37454  cdlemk7  37466  cdlemk11  37467  cdlemk5u  37479  cdlemkj  37481  cdlemkuv2  37485  cdlemk7u  37488  cdlemk11u  37489  cdlemk26-3  37524  cdlemk11t  37564  cdlemk52  37572  cdlemk53a  37573  dihord1  37836  dihord2a  37837  dihord2b  37838  dihord11b  37840  dihord11c  37842  dihord2pre  37843  dihord2pre2  37844  dihord5apre  37880  dihmeetlem1N  37908  dihglblem2N  37912  dihglblem3N  37913  dihglbcpreN  37918  dihmeetlem3N  37923  dihjatc1  37929  suplesup  41068  limsupre  41385  sge0xaddlem2  42179  itscnhlc0yqe  44146  itscnhlc0xyqsol  44152  itsclquadb  44163  itsclquadeu  44164