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  16938  maduf  22863  nllyrest  23712  exatleN  40277  2llnjaN  40439  2lplnja  40492  dalemceb  40511  pclfinN  40773  lhpexle3lem  40884  lhpmcvr5N  40900  lhpmcvr6N  40901  lhp2at0  40905  4atexlemw  40921  cdlemd2  41072  cdlemd4  41074  cdleme7aa  41115  cdleme7c  41118  cdleme7d  41119  cdleme7e  41120  cdleme7ga  41121  cdleme7  41122  cdleme15a  41147  cdleme15b  41148  cdleme15d  41150  cdleme15  41151  cdleme16b  41152  cdleme16c  41153  cdleme16d  41154  cdleme16e  41155  cdleme16f  41156  cdleme18d  41168  cdleme19b  41177  cdleme19d  41179  cdleme19e  41180  cdleme20d  41185  cdleme20e  41186  cdleme20f  41187  cdleme20g  41188  cdleme20h  41189  cdleme20j  41191  cdleme20k  41192  cdleme20l1  41193  cdleme20l2  41194  cdleme20l  41195  cdleme20m  41196  cdleme21c  41200  cdleme21ct  41202  cdleme22cN  41215  cdleme22f  41219  cdleme22g  41221  cdleme23a  41222  cdleme23b  41223  cdleme23c  41224  cdleme25a  41226  cdleme25c  41228  cdleme25dN  41229  cdleme26ee  41233  cdleme26eALTN  41234  cdleme27N  41242  cdleme28a  41243  cdleme28b  41244  cdleme29ex  41247  cdlemefr29exN  41275  cdleme32b  41315  cdleme32c  41316  cdleme32e  41318  cdleme35b  41323  cdleme35c  41324  cdleme35d  41325  cdleme35e  41326  cdleme35f  41327  cdleme42h  41355  cdleme42i  41356  cdleme42k  41357  cdleme48bw  41375  cdlemeg46frv  41398  cdlemeg46vrg  41400  cdlemeg46rgv  41401  cdlemeg46req  41402  cdlemf1  41434  trlord  41442  cdlemg7fvbwN  41480  cdlemg10  41514  cdlemg12e  41520  cdlemg12f  41521  cdlemg19a  41556  cdlemg31c  41572  cdlemg33c0  41575  cdlemg35  41586  tendococl  41645  cdlemh2  41689  cdlemh  41690  cdlemi  41693  cdlemk5  41709  cdlemk7  41721  cdlemk11  41722  cdlemk5u  41734  cdlemkj  41736  cdlemkuv2  41740  cdlemk7u  41743  cdlemk11u  41744  cdlemk26-3  41779  cdlemk11t  41819  cdlemk52  41827  cdlemk53a  41828  dihord1  42091  dihord2a  42092  dihord2b  42093  dihord11b  42095  dihord11c  42097  dihord2pre  42098  dihord2pre2  42099  dihord5apre  42135  dihmeetlem1N  42163  dihglblem2N  42167  dihglblem3N  42168  dihglbcpreN  42173  dihmeetlem3N  42178  dihjatc1  42184  suplesup  46169  limsupre  46469  sge0xaddlem2  47262  itscnhlc0yqe  49689  itscnhlc0xyqsol  49695  itsclquadb  49706  itsclquadeu  49707