Theorem simp11r 1286

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

Assertion

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

Proof of Theorem simp11r

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  pceu  16758  maduf  22557  nllyrest  23402  exatleN  39449  2llnjaN  39611  2lplnja  39664  dalemceb  39683  pclfinN  39945  lhpexle3lem  40056  lhpmcvr5N  40072  lhpmcvr6N  40073  lhp2at0  40077  4atexlemw  40093  cdlemd2  40244  cdlemd4  40246  cdleme7aa  40287  cdleme7c  40290  cdleme7d  40291  cdleme7e  40292  cdleme7ga  40293  cdleme7  40294  cdleme15a  40319  cdleme15b  40320  cdleme15d  40322  cdleme15  40323  cdleme16b  40324  cdleme16c  40325  cdleme16d  40326  cdleme16e  40327  cdleme16f  40328  cdleme18d  40340  cdleme19b  40349  cdleme19d  40351  cdleme19e  40352  cdleme20d  40357  cdleme20e  40358  cdleme20f  40359  cdleme20g  40360  cdleme20h  40361  cdleme20j  40363  cdleme20k  40364  cdleme20l1  40365  cdleme20l2  40366  cdleme20l  40367  cdleme20m  40368  cdleme21c  40372  cdleme21ct  40374  cdleme22cN  40387  cdleme22f  40391  cdleme22g  40393  cdleme23a  40394  cdleme23b  40395  cdleme23c  40396  cdleme25a  40398  cdleme25c  40400  cdleme25dN  40401  cdleme26ee  40405  cdleme26eALTN  40406  cdleme27N  40414  cdleme28a  40415  cdleme28b  40416  cdleme29ex  40419  cdlemefr29exN  40447  cdleme32b  40487  cdleme32c  40488  cdleme32e  40490  cdleme35b  40495  cdleme35c  40496  cdleme35d  40497  cdleme35e  40498  cdleme35f  40499  cdleme42h  40527  cdleme42i  40528  cdleme42k  40529  cdleme48bw  40547  cdlemeg46frv  40570  cdlemeg46vrg  40572  cdlemeg46rgv  40573  cdlemeg46req  40574  cdlemf1  40606  trlord  40614  cdlemg7fvbwN  40652  cdlemg10  40686  cdlemg12e  40692  cdlemg12f  40693  cdlemg19a  40728  cdlemg31c  40744  cdlemg33c0  40747  cdlemg35  40758  tendococl  40817  cdlemh2  40861  cdlemh  40862  cdlemi  40865  cdlemk5  40881  cdlemk7  40893  cdlemk11  40894  cdlemk5u  40906  cdlemkj  40908  cdlemkuv2  40912  cdlemk7u  40915  cdlemk11u  40916  cdlemk26-3  40951  cdlemk11t  40991  cdlemk52  40999  cdlemk53a  41000  dihord1  41263  dihord2a  41264  dihord2b  41265  dihord11b  41267  dihord11c  41269  dihord2pre  41270  dihord2pre2  41271  dihord5apre  41307  dihmeetlem1N  41335  dihglblem2N  41339  dihglblem3N  41340  dihglbcpreN  41345  dihmeetlem3N  41350  dihjatc1  41356  suplesup  45384  limsupre  45685  sge0xaddlem2  46478  itscnhlc0yqe  48797  itscnhlc0xyqsol  48803  itsclquadb  48814  itsclquadeu  48815