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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  pceu  16907  maduf  22779  nllyrest  23624  exatleN  40159  2llnjaN  40321  2lplnja  40374  dalemceb  40393  pclfinN  40655  lhpexle3lem  40766  lhpmcvr5N  40782  lhpmcvr6N  40783  lhp2at0  40787  4atexlemw  40803  cdlemd2  40954  cdlemd4  40956  cdleme7aa  40997  cdleme7c  41000  cdleme7d  41001  cdleme7e  41002  cdleme7ga  41003  cdleme7  41004  cdleme15a  41029  cdleme15b  41030  cdleme15d  41032  cdleme15  41033  cdleme16b  41034  cdleme16c  41035  cdleme16d  41036  cdleme16e  41037  cdleme16f  41038  cdleme18d  41050  cdleme19b  41059  cdleme19d  41061  cdleme19e  41062  cdleme20d  41067  cdleme20e  41068  cdleme20f  41069  cdleme20g  41070  cdleme20h  41071  cdleme20j  41073  cdleme20k  41074  cdleme20l1  41075  cdleme20l2  41076  cdleme20l  41077  cdleme20m  41078  cdleme21c  41082  cdleme21ct  41084  cdleme22cN  41097  cdleme22f  41101  cdleme22g  41103  cdleme23a  41104  cdleme23b  41105  cdleme23c  41106  cdleme25a  41108  cdleme25c  41110  cdleme25dN  41111  cdleme26ee  41115  cdleme26eALTN  41116  cdleme27N  41124  cdleme28a  41125  cdleme28b  41126  cdleme29ex  41129  cdlemefr29exN  41157  cdleme32b  41197  cdleme32c  41198  cdleme32e  41200  cdleme35b  41205  cdleme35c  41206  cdleme35d  41207  cdleme35e  41208  cdleme35f  41209  cdleme42h  41237  cdleme42i  41238  cdleme42k  41239  cdleme48bw  41257  cdlemeg46frv  41280  cdlemeg46vrg  41282  cdlemeg46rgv  41283  cdlemeg46req  41284  cdlemf1  41316  trlord  41324  cdlemg7fvbwN  41362  cdlemg10  41396  cdlemg12e  41402  cdlemg12f  41403  cdlemg19a  41438  cdlemg31c  41454  cdlemg33c0  41457  cdlemg35  41468  tendococl  41527  cdlemh2  41571  cdlemh  41572  cdlemi  41575  cdlemk5  41591  cdlemk7  41603  cdlemk11  41604  cdlemk5u  41616  cdlemkj  41618  cdlemkuv2  41622  cdlemk7u  41625  cdlemk11u  41626  cdlemk26-3  41661  cdlemk11t  41701  cdlemk52  41709  cdlemk53a  41710  dihord1  41973  dihord2a  41974  dihord2b  41975  dihord11b  41977  dihord11c  41979  dihord2pre  41980  dihord2pre2  41981  dihord5apre  42017  dihmeetlem1N  42045  dihglblem2N  42049  dihglblem3N  42050  dihglbcpreN  42055  dihmeetlem3N  42060  dihjatc1  42066  suplesup  46038  limsupre  46338  sge0xaddlem2  47131  itscnhlc0yqe  49522  itscnhlc0xyqsol  49528  itsclquadb  49539  itsclquadeu  49540