Theorem simp11r 1287

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

Assertion

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

Proof of Theorem simp11r

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

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

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 1089

This theorem is referenced by:  pceu  16817  maduf  22606  nllyrest  23451  exatleN  39850  2llnjaN  40012  2lplnja  40065  dalemceb  40084  pclfinN  40346  lhpexle3lem  40457  lhpmcvr5N  40473  lhpmcvr6N  40474  lhp2at0  40478  4atexlemw  40494  cdlemd2  40645  cdlemd4  40647  cdleme7aa  40688  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme15a  40720  cdleme15b  40721  cdleme15d  40723  cdleme15  40724  cdleme16b  40725  cdleme16c  40726  cdleme16d  40727  cdleme16e  40728  cdleme16f  40729  cdleme18d  40741  cdleme19b  40750  cdleme19d  40752  cdleme19e  40753  cdleme20d  40758  cdleme20e  40759  cdleme20f  40760  cdleme20g  40761  cdleme20h  40762  cdleme20j  40764  cdleme20k  40765  cdleme20l1  40766  cdleme20l2  40767  cdleme20l  40768  cdleme20m  40769  cdleme21c  40773  cdleme21ct  40775  cdleme22cN  40788  cdleme22f  40792  cdleme22g  40794  cdleme23a  40795  cdleme23b  40796  cdleme23c  40797  cdleme25a  40799  cdleme25c  40801  cdleme25dN  40802  cdleme26ee  40806  cdleme26eALTN  40807  cdleme27N  40815  cdleme28a  40816  cdleme28b  40817  cdleme29ex  40820  cdlemefr29exN  40848  cdleme32b  40888  cdleme32c  40889  cdleme32e  40891  cdleme35b  40896  cdleme35c  40897  cdleme35d  40898  cdleme35e  40899  cdleme35f  40900  cdleme42h  40928  cdleme42i  40929  cdleme42k  40930  cdleme48bw  40948  cdlemeg46frv  40971  cdlemeg46vrg  40973  cdlemeg46rgv  40974  cdlemeg46req  40975  cdlemf1  41007  trlord  41015  cdlemg7fvbwN  41053  cdlemg10  41087  cdlemg12e  41093  cdlemg12f  41094  cdlemg19a  41129  cdlemg31c  41145  cdlemg33c0  41148  cdlemg35  41159  tendococl  41218  cdlemh2  41262  cdlemh  41263  cdlemi  41266  cdlemk5  41282  cdlemk7  41294  cdlemk11  41295  cdlemk5u  41307  cdlemkj  41309  cdlemkuv2  41313  cdlemk7u  41316  cdlemk11u  41317  cdlemk26-3  41352  cdlemk11t  41392  cdlemk52  41400  cdlemk53a  41401  dihord1  41664  dihord2a  41665  dihord2b  41666  dihord11b  41668  dihord11c  41670  dihord2pre  41671  dihord2pre2  41672  dihord5apre  41708  dihmeetlem1N  41736  dihglblem2N  41740  dihglblem3N  41741  dihglbcpreN  41746  dihmeetlem3N  41751  dihjatc1  41757  suplesup  45769  limsupre  46069  sge0xaddlem2  46862  itscnhlc0yqe  49235  itscnhlc0xyqsol  49241  itsclquadb  49252  itsclquadeu  49253