Theorem simp11r 1304

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

Assertion

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

Proof of Theorem simp11r

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pceu  17030  maduf  22962  nllyrest  23811  exatleN  40555  2llnjaN  40717  2lplnja  40770  dalemceb  40789  pclfinN  41051  lhpexle3lem  41162  lhpmcvr5N  41178  lhpmcvr6N  41179  lhp2at0  41183  4atexlemw  41199  cdlemd2  41350  cdlemd4  41352  cdleme7aa  41393  cdleme7c  41396  cdleme7d  41397  cdleme7e  41398  cdleme7ga  41399  cdleme7  41400  cdleme15a  41425  cdleme15b  41426  cdleme15d  41428  cdleme15  41429  cdleme16b  41430  cdleme16c  41431  cdleme16d  41432  cdleme16e  41433  cdleme16f  41434  cdleme18d  41446  cdleme19b  41455  cdleme19d  41457  cdleme19e  41458  cdleme20d  41463  cdleme20e  41464  cdleme20f  41465  cdleme20g  41466  cdleme20h  41467  cdleme20j  41469  cdleme20k  41470  cdleme20l1  41471  cdleme20l2  41472  cdleme20l  41473  cdleme20m  41474  cdleme21c  41478  cdleme21ct  41480  cdleme22cN  41493  cdleme22f  41497  cdleme22g  41499  cdleme23a  41500  cdleme23b  41501  cdleme23c  41502  cdleme25a  41504  cdleme25c  41506  cdleme25dN  41507  cdleme26ee  41511  cdleme26eALTN  41512  cdleme27N  41520  cdleme28a  41521  cdleme28b  41522  cdleme29ex  41525  cdlemefr29exN  41553  cdleme32b  41593  cdleme32c  41594  cdleme32e  41596  cdleme35b  41601  cdleme35c  41602  cdleme35d  41603  cdleme35e  41604  cdleme35f  41605  cdleme42h  41633  cdleme42i  41634  cdleme42k  41635  cdleme48bw  41653  cdlemeg46frv  41676  cdlemeg46vrg  41678  cdlemeg46rgv  41679  cdlemeg46req  41680  cdlemf1  41712  trlord  41720  cdlemg7fvbwN  41758  cdlemg10  41792  cdlemg12e  41798  cdlemg12f  41799  cdlemg19a  41834  cdlemg31c  41850  cdlemg33c0  41853  cdlemg35  41864  tendococl  41923  cdlemh2  41967  cdlemh  41968  cdlemi  41971  cdlemk5  41987  cdlemk7  41999  cdlemk11  42000  cdlemk5u  42012  cdlemkj  42014  cdlemkuv2  42018  cdlemk7u  42021  cdlemk11u  42022  cdlemk26-3  42057  cdlemk11t  42097  cdlemk52  42105  cdlemk53a  42106  dihord1  42369  dihord2a  42370  dihord2b  42371  dihord11b  42373  dihord11c  42375  dihord2pre  42376  dihord2pre2  42377  dihord5apre  42413  dihmeetlem1N  42441  dihglblem2N  42445  dihglblem3N  42446  dihglbcpreN  42451  dihmeetlem3N  42456  dihjatc1  42462  suplesup  46445  limsupre  46745  sge0xaddlem2  47538  itscnhlc0yqe  49965  itscnhlc0xyqsol  49971  itsclquadb  49982  itsclquadeu  49983