Theorem simp11r 1298

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

Assertion

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

Proof of Theorem simp11r

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  pceu  16872  maduf  22688  nllyrest  23533  exatleN  39988  2llnjaN  40150  2lplnja  40203  dalemceb  40222  pclfinN  40484  lhpexle3lem  40595  lhpmcvr5N  40611  lhpmcvr6N  40612  lhp2at0  40616  4atexlemw  40632  cdlemd2  40783  cdlemd4  40785  cdleme7aa  40826  cdleme7c  40829  cdleme7d  40830  cdleme7e  40831  cdleme7ga  40832  cdleme7  40833  cdleme15a  40858  cdleme15b  40859  cdleme15d  40861  cdleme15  40862  cdleme16b  40863  cdleme16c  40864  cdleme16d  40865  cdleme16e  40866  cdleme16f  40867  cdleme18d  40879  cdleme19b  40888  cdleme19d  40890  cdleme19e  40891  cdleme20d  40896  cdleme20e  40897  cdleme20f  40898  cdleme20g  40899  cdleme20h  40900  cdleme20j  40902  cdleme20k  40903  cdleme20l1  40904  cdleme20l2  40905  cdleme20l  40906  cdleme20m  40907  cdleme21c  40911  cdleme21ct  40913  cdleme22cN  40926  cdleme22f  40930  cdleme22g  40932  cdleme23a  40933  cdleme23b  40934  cdleme23c  40935  cdleme25a  40937  cdleme25c  40939  cdleme25dN  40940  cdleme26ee  40944  cdleme26eALTN  40945  cdleme27N  40953  cdleme28a  40954  cdleme28b  40955  cdleme29ex  40958  cdlemefr29exN  40986  cdleme32b  41026  cdleme32c  41027  cdleme32e  41029  cdleme35b  41034  cdleme35c  41035  cdleme35d  41036  cdleme35e  41037  cdleme35f  41038  cdleme42h  41066  cdleme42i  41067  cdleme42k  41068  cdleme48bw  41086  cdlemeg46frv  41109  cdlemeg46vrg  41111  cdlemeg46rgv  41112  cdlemeg46req  41113  cdlemf1  41145  trlord  41153  cdlemg7fvbwN  41191  cdlemg10  41225  cdlemg12e  41231  cdlemg12f  41232  cdlemg19a  41267  cdlemg31c  41283  cdlemg33c0  41286  cdlemg35  41297  tendococl  41356  cdlemh2  41400  cdlemh  41401  cdlemi  41404  cdlemk5  41420  cdlemk7  41432  cdlemk11  41433  cdlemk5u  41445  cdlemkj  41447  cdlemkuv2  41451  cdlemk7u  41454  cdlemk11u  41455  cdlemk26-3  41490  cdlemk11t  41530  cdlemk52  41538  cdlemk53a  41539  dihord1  41802  dihord2a  41803  dihord2b  41804  dihord11b  41806  dihord11c  41808  dihord2pre  41809  dihord2pre2  41810  dihord5apre  41846  dihmeetlem1N  41874  dihglblem2N  41878  dihglblem3N  41879  dihglbcpreN  41884  dihmeetlem3N  41889  dihjatc1  41895  suplesup  45875  limsupre  46175  sge0xaddlem2  46968  itscnhlc0yqe  49341  itscnhlc0xyqsol  49347  itsclquadb  49358  itsclquadeu  49359