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 1135	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓)

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

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  pceu  16362  maduf  21492  nllyrest  22337  exatleN  37104  2llnjaN  37266  2lplnja  37319  dalemceb  37338  pclfinN  37600  lhpexle3lem  37711  lhpmcvr5N  37727  lhpmcvr6N  37728  lhp2at0  37732  4atexlemw  37748  cdlemd2  37899  cdlemd4  37901  cdleme7aa  37942  cdleme7c  37945  cdleme7d  37946  cdleme7e  37947  cdleme7ga  37948  cdleme7  37949  cdleme15a  37974  cdleme15b  37975  cdleme15d  37977  cdleme15  37978  cdleme16b  37979  cdleme16c  37980  cdleme16d  37981  cdleme16e  37982  cdleme16f  37983  cdleme18d  37995  cdleme19b  38004  cdleme19d  38006  cdleme19e  38007  cdleme20d  38012  cdleme20e  38013  cdleme20f  38014  cdleme20g  38015  cdleme20h  38016  cdleme20j  38018  cdleme20k  38019  cdleme20l1  38020  cdleme20l2  38021  cdleme20l  38022  cdleme20m  38023  cdleme21c  38027  cdleme21ct  38029  cdleme22cN  38042  cdleme22f  38046  cdleme22g  38048  cdleme23a  38049  cdleme23b  38050  cdleme23c  38051  cdleme25a  38053  cdleme25c  38055  cdleme25dN  38056  cdleme26ee  38060  cdleme26eALTN  38061  cdleme27N  38069  cdleme28a  38070  cdleme28b  38071  cdleme29ex  38074  cdlemefr29exN  38102  cdleme32b  38142  cdleme32c  38143  cdleme32e  38145  cdleme35b  38150  cdleme35c  38151  cdleme35d  38152  cdleme35e  38153  cdleme35f  38154  cdleme42h  38182  cdleme42i  38183  cdleme42k  38184  cdleme48bw  38202  cdlemeg46frv  38225  cdlemeg46vrg  38227  cdlemeg46rgv  38228  cdlemeg46req  38229  cdlemf1  38261  trlord  38269  cdlemg7fvbwN  38307  cdlemg10  38341  cdlemg12e  38347  cdlemg12f  38348  cdlemg19a  38383  cdlemg31c  38399  cdlemg33c0  38402  cdlemg35  38413  tendococl  38472  cdlemh2  38516  cdlemh  38517  cdlemi  38520  cdlemk5  38536  cdlemk7  38548  cdlemk11  38549  cdlemk5u  38561  cdlemkj  38563  cdlemkuv2  38567  cdlemk7u  38570  cdlemk11u  38571  cdlemk26-3  38606  cdlemk11t  38646  cdlemk52  38654  cdlemk53a  38655  dihord1  38918  dihord2a  38919  dihord2b  38920  dihord11b  38922  dihord11c  38924  dihord2pre  38925  dihord2pre2  38926  dihord5apre  38962  dihmeetlem1N  38990  dihglblem2N  38994  dihglblem3N  38995  dihglbcpreN  39000  dihmeetlem3N  39005  dihjatc1  39011  suplesup  42492  limsupre  42800  sge0xaddlem2  43590  itscnhlc0yqe  45721  itscnhlc0xyqsol  45727  itsclquadb  45738  itsclquadeu  45739