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  16817  maduf  22528  nllyrest  23373  exatleN  39398  2llnjaN  39560  2lplnja  39613  dalemceb  39632  pclfinN  39894  lhpexle3lem  40005  lhpmcvr5N  40021  lhpmcvr6N  40022  lhp2at0  40026  4atexlemw  40042  cdlemd2  40193  cdlemd4  40195  cdleme7aa  40236  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme15a  40268  cdleme15b  40269  cdleme15d  40271  cdleme15  40272  cdleme16b  40273  cdleme16c  40274  cdleme16d  40275  cdleme16e  40276  cdleme16f  40277  cdleme18d  40289  cdleme19b  40298  cdleme19d  40300  cdleme19e  40301  cdleme20d  40306  cdleme20e  40307  cdleme20f  40308  cdleme20g  40309  cdleme20h  40310  cdleme20j  40312  cdleme20k  40313  cdleme20l1  40314  cdleme20l2  40315  cdleme20l  40316  cdleme20m  40317  cdleme21c  40321  cdleme21ct  40323  cdleme22cN  40336  cdleme22f  40340  cdleme22g  40342  cdleme23a  40343  cdleme23b  40344  cdleme23c  40345  cdleme25a  40347  cdleme25c  40349  cdleme25dN  40350  cdleme26ee  40354  cdleme26eALTN  40355  cdleme27N  40363  cdleme28a  40364  cdleme28b  40365  cdleme29ex  40368  cdlemefr29exN  40396  cdleme32b  40436  cdleme32c  40437  cdleme32e  40439  cdleme35b  40444  cdleme35c  40445  cdleme35d  40446  cdleme35e  40447  cdleme35f  40448  cdleme42h  40476  cdleme42i  40477  cdleme42k  40478  cdleme48bw  40496  cdlemeg46frv  40519  cdlemeg46vrg  40521  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemf1  40555  trlord  40563  cdlemg7fvbwN  40601  cdlemg10  40635  cdlemg12e  40641  cdlemg12f  40642  cdlemg19a  40677  cdlemg31c  40693  cdlemg33c0  40696  cdlemg35  40707  tendococl  40766  cdlemh2  40810  cdlemh  40811  cdlemi  40814  cdlemk5  40830  cdlemk7  40842  cdlemk11  40843  cdlemk5u  40855  cdlemkj  40857  cdlemkuv2  40861  cdlemk7u  40864  cdlemk11u  40865  cdlemk26-3  40900  cdlemk11t  40940  cdlemk52  40948  cdlemk53a  40949  dihord1  41212  dihord2a  41213  dihord2b  41214  dihord11b  41216  dihord11c  41218  dihord2pre  41219  dihord2pre2  41220  dihord5apre  41256  dihmeetlem1N  41284  dihglblem2N  41288  dihglblem3N  41289  dihglbcpreN  41294  dihmeetlem3N  41299  dihjatc1  41305  suplesup  45335  limsupre  45639  sge0xaddlem2  46432  itscnhlc0yqe  48748  itscnhlc0xyqsol  48754  itsclquadb  48765  itsclquadeu  48766