Theorem simp11r 1287

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

Assertion

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

Proof of Theorem simp11r

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

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

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 1089

This theorem is referenced by:  pceu  16808  maduf  22616  nllyrest  23461  exatleN  39864  2llnjaN  40026  2lplnja  40079  dalemceb  40098  pclfinN  40360  lhpexle3lem  40471  lhpmcvr5N  40487  lhpmcvr6N  40488  lhp2at0  40492  4atexlemw  40508  cdlemd2  40659  cdlemd4  40661  cdleme7aa  40702  cdleme7c  40705  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme7  40709  cdleme15a  40734  cdleme15b  40735  cdleme15d  40737  cdleme15  40738  cdleme16b  40739  cdleme16c  40740  cdleme16d  40741  cdleme16e  40742  cdleme16f  40743  cdleme18d  40755  cdleme19b  40764  cdleme19d  40766  cdleme19e  40767  cdleme20d  40772  cdleme20e  40773  cdleme20f  40774  cdleme20g  40775  cdleme20h  40776  cdleme20j  40778  cdleme20k  40779  cdleme20l1  40780  cdleme20l2  40781  cdleme20l  40782  cdleme20m  40783  cdleme21c  40787  cdleme21ct  40789  cdleme22cN  40802  cdleme22f  40806  cdleme22g  40808  cdleme23a  40809  cdleme23b  40810  cdleme23c  40811  cdleme25a  40813  cdleme25c  40815  cdleme25dN  40816  cdleme26ee  40820  cdleme26eALTN  40821  cdleme27N  40829  cdleme28a  40830  cdleme28b  40831  cdleme29ex  40834  cdlemefr29exN  40862  cdleme32b  40902  cdleme32c  40903  cdleme32e  40905  cdleme35b  40910  cdleme35c  40911  cdleme35d  40912  cdleme35e  40913  cdleme35f  40914  cdleme42h  40942  cdleme42i  40943  cdleme42k  40944  cdleme48bw  40962  cdlemeg46frv  40985  cdlemeg46vrg  40987  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemf1  41021  trlord  41029  cdlemg7fvbwN  41067  cdlemg10  41101  cdlemg12e  41107  cdlemg12f  41108  cdlemg19a  41143  cdlemg31c  41159  cdlemg33c0  41162  cdlemg35  41173  tendococl  41232  cdlemh2  41276  cdlemh  41277  cdlemi  41280  cdlemk5  41296  cdlemk7  41308  cdlemk11  41309  cdlemk5u  41321  cdlemkj  41323  cdlemkuv2  41327  cdlemk7u  41330  cdlemk11u  41331  cdlemk26-3  41366  cdlemk11t  41406  cdlemk52  41414  cdlemk53a  41415  dihord1  41678  dihord2a  41679  dihord2b  41680  dihord11b  41682  dihord11c  41684  dihord2pre  41685  dihord2pre2  41686  dihord5apre  41722  dihmeetlem1N  41750  dihglblem2N  41754  dihglblem3N  41755  dihglbcpreN  41760  dihmeetlem3N  41765  dihjatc1  41771  suplesup  45787  limsupre  46087  sge0xaddlem2  46880  itscnhlc0yqe  49247  itscnhlc0xyqsol  49253  itsclquadb  49264  itsclquadeu  49265