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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pceu  16923  maduf  22827  nllyrest  23672  exatleN  40211  2llnjaN  40373  2lplnja  40426  dalemceb  40445  pclfinN  40707  lhpexle3lem  40818  lhpmcvr5N  40834  lhpmcvr6N  40835  lhp2at0  40839  4atexlemw  40855  cdlemd2  41006  cdlemd4  41008  cdleme7aa  41049  cdleme7c  41052  cdleme7d  41053  cdleme7e  41054  cdleme7ga  41055  cdleme7  41056  cdleme15a  41081  cdleme15b  41082  cdleme15d  41084  cdleme15  41085  cdleme16b  41086  cdleme16c  41087  cdleme16d  41088  cdleme16e  41089  cdleme16f  41090  cdleme18d  41102  cdleme19b  41111  cdleme19d  41113  cdleme19e  41114  cdleme20d  41119  cdleme20e  41120  cdleme20f  41121  cdleme20g  41122  cdleme20h  41123  cdleme20j  41125  cdleme20k  41126  cdleme20l1  41127  cdleme20l2  41128  cdleme20l  41129  cdleme20m  41130  cdleme21c  41134  cdleme21ct  41136  cdleme22cN  41149  cdleme22f  41153  cdleme22g  41155  cdleme23a  41156  cdleme23b  41157  cdleme23c  41158  cdleme25a  41160  cdleme25c  41162  cdleme25dN  41163  cdleme26ee  41167  cdleme26eALTN  41168  cdleme27N  41176  cdleme28a  41177  cdleme28b  41178  cdleme29ex  41181  cdlemefr29exN  41209  cdleme32b  41249  cdleme32c  41250  cdleme32e  41252  cdleme35b  41257  cdleme35c  41258  cdleme35d  41259  cdleme35e  41260  cdleme35f  41261  cdleme42h  41289  cdleme42i  41290  cdleme42k  41291  cdleme48bw  41309  cdlemeg46frv  41332  cdlemeg46vrg  41334  cdlemeg46rgv  41335  cdlemeg46req  41336  cdlemf1  41368  trlord  41376  cdlemg7fvbwN  41414  cdlemg10  41448  cdlemg12e  41454  cdlemg12f  41455  cdlemg19a  41490  cdlemg31c  41506  cdlemg33c0  41509  cdlemg35  41520  tendococl  41579  cdlemh2  41623  cdlemh  41624  cdlemi  41627  cdlemk5  41643  cdlemk7  41655  cdlemk11  41656  cdlemk5u  41668  cdlemkj  41670  cdlemkuv2  41674  cdlemk7u  41677  cdlemk11u  41678  cdlemk26-3  41713  cdlemk11t  41753  cdlemk52  41761  cdlemk53a  41762  dihord1  42025  dihord2a  42026  dihord2b  42027  dihord11b  42029  dihord11c  42031  dihord2pre  42032  dihord2pre2  42033  dihord5apre  42069  dihmeetlem1N  42097  dihglblem2N  42101  dihglblem3N  42102  dihglbcpreN  42107  dihmeetlem3N  42112  dihjatc1  42118  suplesup  46088  limsupre  46388  sge0xaddlem2  47181  itscnhlc0yqe  49572  itscnhlc0xyqsol  49578  itsclquadb  49589  itsclquadeu  49590