Theorem simp11r 1293

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

Assertion

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

Proof of Theorem simp11r

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  pceu  16812  maduf  22628  nllyrest  23473  exatleN  39911  2llnjaN  40073  2lplnja  40126  dalemceb  40145  pclfinN  40407  lhpexle3lem  40518  lhpmcvr5N  40534  lhpmcvr6N  40535  lhp2at0  40539  4atexlemw  40555  cdlemd2  40706  cdlemd4  40708  cdleme7aa  40749  cdleme7c  40752  cdleme7d  40753  cdleme7e  40754  cdleme7ga  40755  cdleme7  40756  cdleme15a  40781  cdleme15b  40782  cdleme15d  40784  cdleme15  40785  cdleme16b  40786  cdleme16c  40787  cdleme16d  40788  cdleme16e  40789  cdleme16f  40790  cdleme18d  40802  cdleme19b  40811  cdleme19d  40813  cdleme19e  40814  cdleme20d  40819  cdleme20e  40820  cdleme20f  40821  cdleme20g  40822  cdleme20h  40823  cdleme20j  40825  cdleme20k  40826  cdleme20l1  40827  cdleme20l2  40828  cdleme20l  40829  cdleme20m  40830  cdleme21c  40834  cdleme21ct  40836  cdleme22cN  40849  cdleme22f  40853  cdleme22g  40855  cdleme23a  40856  cdleme23b  40857  cdleme23c  40858  cdleme25a  40860  cdleme25c  40862  cdleme25dN  40863  cdleme26ee  40867  cdleme26eALTN  40868  cdleme27N  40876  cdleme28a  40877  cdleme28b  40878  cdleme29ex  40881  cdlemefr29exN  40909  cdleme32b  40949  cdleme32c  40950  cdleme32e  40952  cdleme35b  40957  cdleme35c  40958  cdleme35d  40959  cdleme35e  40960  cdleme35f  40961  cdleme42h  40989  cdleme42i  40990  cdleme42k  40991  cdleme48bw  41009  cdlemeg46frv  41032  cdlemeg46vrg  41034  cdlemeg46rgv  41035  cdlemeg46req  41036  cdlemf1  41068  trlord  41076  cdlemg7fvbwN  41114  cdlemg10  41148  cdlemg12e  41154  cdlemg12f  41155  cdlemg19a  41190  cdlemg31c  41206  cdlemg33c0  41209  cdlemg35  41220  tendococl  41279  cdlemh2  41323  cdlemh  41324  cdlemi  41327  cdlemk5  41343  cdlemk7  41355  cdlemk11  41356  cdlemk5u  41368  cdlemkj  41370  cdlemkuv2  41374  cdlemk7u  41377  cdlemk11u  41378  cdlemk26-3  41413  cdlemk11t  41453  cdlemk52  41461  cdlemk53a  41462  dihord1  41725  dihord2a  41726  dihord2b  41727  dihord11b  41729  dihord11c  41731  dihord2pre  41732  dihord2pre2  41733  dihord5apre  41769  dihmeetlem1N  41797  dihglblem2N  41801  dihglblem3N  41802  dihglbcpreN  41807  dihmeetlem3N  41812  dihjatc1  41818  suplesup  45798  limsupre  46098  sge0xaddlem2  46891  itscnhlc0yqe  49264  itscnhlc0xyqsol  49270  itsclquadb  49281  itsclquadeu  49282