Theorem simp11r 1284

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

Assertion

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

Proof of Theorem simp11r

Step	Hyp	Ref	Expression
1		simp1r 1197	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant1 1132	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  16879  maduf  22662  nllyrest  23509  exatleN  39386  2llnjaN  39548  2lplnja  39601  dalemceb  39620  pclfinN  39882  lhpexle3lem  39993  lhpmcvr5N  40009  lhpmcvr6N  40010  lhp2at0  40014  4atexlemw  40030  cdlemd2  40181  cdlemd4  40183  cdleme7aa  40224  cdleme7c  40227  cdleme7d  40228  cdleme7e  40229  cdleme7ga  40230  cdleme7  40231  cdleme15a  40256  cdleme15b  40257  cdleme15d  40259  cdleme15  40260  cdleme16b  40261  cdleme16c  40262  cdleme16d  40263  cdleme16e  40264  cdleme16f  40265  cdleme18d  40277  cdleme19b  40286  cdleme19d  40288  cdleme19e  40289  cdleme20d  40294  cdleme20e  40295  cdleme20f  40296  cdleme20g  40297  cdleme20h  40298  cdleme20j  40300  cdleme20k  40301  cdleme20l1  40302  cdleme20l2  40303  cdleme20l  40304  cdleme20m  40305  cdleme21c  40309  cdleme21ct  40311  cdleme22cN  40324  cdleme22f  40328  cdleme22g  40330  cdleme23a  40331  cdleme23b  40332  cdleme23c  40333  cdleme25a  40335  cdleme25c  40337  cdleme25dN  40338  cdleme26ee  40342  cdleme26eALTN  40343  cdleme27N  40351  cdleme28a  40352  cdleme28b  40353  cdleme29ex  40356  cdlemefr29exN  40384  cdleme32b  40424  cdleme32c  40425  cdleme32e  40427  cdleme35b  40432  cdleme35c  40433  cdleme35d  40434  cdleme35e  40435  cdleme35f  40436  cdleme42h  40464  cdleme42i  40465  cdleme42k  40466  cdleme48bw  40484  cdlemeg46frv  40507  cdlemeg46vrg  40509  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemf1  40543  trlord  40551  cdlemg7fvbwN  40589  cdlemg10  40623  cdlemg12e  40629  cdlemg12f  40630  cdlemg19a  40665  cdlemg31c  40681  cdlemg33c0  40684  cdlemg35  40695  tendococl  40754  cdlemh2  40798  cdlemh  40799  cdlemi  40802  cdlemk5  40818  cdlemk7  40830  cdlemk11  40831  cdlemk5u  40843  cdlemkj  40845  cdlemkuv2  40849  cdlemk7u  40852  cdlemk11u  40853  cdlemk26-3  40888  cdlemk11t  40928  cdlemk52  40936  cdlemk53a  40937  dihord1  41200  dihord2a  41201  dihord2b  41202  dihord11b  41204  dihord11c  41206  dihord2pre  41207  dihord2pre2  41208  dihord5apre  41244  dihmeetlem1N  41272  dihglblem2N  41276  dihglblem3N  41277  dihglbcpreN  41282  dihmeetlem3N  41287  dihjatc1  41293  suplesup  45288  limsupre  45596  sge0xaddlem2  46389  itscnhlc0yqe  48608  itscnhlc0xyqsol  48614  itsclquadb  48625  itsclquadeu  48626