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  16866  maduf  22579  nllyrest  23424  exatleN  39423  2llnjaN  39585  2lplnja  39638  dalemceb  39657  pclfinN  39919  lhpexle3lem  40030  lhpmcvr5N  40046  lhpmcvr6N  40047  lhp2at0  40051  4atexlemw  40067  cdlemd2  40218  cdlemd4  40220  cdleme7aa  40261  cdleme7c  40264  cdleme7d  40265  cdleme7e  40266  cdleme7ga  40267  cdleme7  40268  cdleme15a  40293  cdleme15b  40294  cdleme15d  40296  cdleme15  40297  cdleme16b  40298  cdleme16c  40299  cdleme16d  40300  cdleme16e  40301  cdleme16f  40302  cdleme18d  40314  cdleme19b  40323  cdleme19d  40325  cdleme19e  40326  cdleme20d  40331  cdleme20e  40332  cdleme20f  40333  cdleme20g  40334  cdleme20h  40335  cdleme20j  40337  cdleme20k  40338  cdleme20l1  40339  cdleme20l2  40340  cdleme20l  40341  cdleme20m  40342  cdleme21c  40346  cdleme21ct  40348  cdleme22cN  40361  cdleme22f  40365  cdleme22g  40367  cdleme23a  40368  cdleme23b  40369  cdleme23c  40370  cdleme25a  40372  cdleme25c  40374  cdleme25dN  40375  cdleme26ee  40379  cdleme26eALTN  40380  cdleme27N  40388  cdleme28a  40389  cdleme28b  40390  cdleme29ex  40393  cdlemefr29exN  40421  cdleme32b  40461  cdleme32c  40462  cdleme32e  40464  cdleme35b  40469  cdleme35c  40470  cdleme35d  40471  cdleme35e  40472  cdleme35f  40473  cdleme42h  40501  cdleme42i  40502  cdleme42k  40503  cdleme48bw  40521  cdlemeg46frv  40544  cdlemeg46vrg  40546  cdlemeg46rgv  40547  cdlemeg46req  40548  cdlemf1  40580  trlord  40588  cdlemg7fvbwN  40626  cdlemg10  40660  cdlemg12e  40666  cdlemg12f  40667  cdlemg19a  40702  cdlemg31c  40718  cdlemg33c0  40721  cdlemg35  40732  tendococl  40791  cdlemh2  40835  cdlemh  40836  cdlemi  40839  cdlemk5  40855  cdlemk7  40867  cdlemk11  40868  cdlemk5u  40880  cdlemkj  40882  cdlemkuv2  40886  cdlemk7u  40889  cdlemk11u  40890  cdlemk26-3  40925  cdlemk11t  40965  cdlemk52  40973  cdlemk53a  40974  dihord1  41237  dihord2a  41238  dihord2b  41239  dihord11b  41241  dihord11c  41243  dihord2pre  41244  dihord2pre2  41245  dihord5apre  41281  dihmeetlem1N  41309  dihglblem2N  41313  dihglblem3N  41314  dihglbcpreN  41319  dihmeetlem3N  41324  dihjatc1  41330  suplesup  45366  limsupre  45670  sge0xaddlem2  46463  itscnhlc0yqe  48739  itscnhlc0xyqsol  48745  itsclquadb  48756  itsclquadeu  48757