Theorem simp11r 1304

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

Assertion

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

Proof of Theorem simp11r

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pceu  17068  maduf  23011  nllyrest  23860  exatleN  40727  2llnjaN  40889  2lplnja  40942  dalemceb  40961  pclfinN  41223  lhpexle3lem  41334  lhpmcvr5N  41350  lhpmcvr6N  41351  lhp2at0  41355  4atexlemw  41371  cdlemd2  41522  cdlemd4  41524  cdleme7aa  41565  cdleme7c  41568  cdleme7d  41569  cdleme7e  41570  cdleme7ga  41571  cdleme7  41572  cdleme15a  41597  cdleme15b  41598  cdleme15d  41600  cdleme15  41601  cdleme16b  41602  cdleme16c  41603  cdleme16d  41604  cdleme16e  41605  cdleme16f  41606  cdleme18d  41618  cdleme19b  41627  cdleme19d  41629  cdleme19e  41630  cdleme20d  41635  cdleme20e  41636  cdleme20f  41637  cdleme20g  41638  cdleme20h  41639  cdleme20j  41641  cdleme20k  41642  cdleme20l1  41643  cdleme20l2  41644  cdleme20l  41645  cdleme20m  41646  cdleme21c  41650  cdleme21ct  41652  cdleme22cN  41665  cdleme22f  41669  cdleme22g  41671  cdleme23a  41672  cdleme23b  41673  cdleme23c  41674  cdleme25a  41676  cdleme25c  41678  cdleme25dN  41679  cdleme26ee  41683  cdleme26eALTN  41684  cdleme27N  41692  cdleme28a  41693  cdleme28b  41694  cdleme29ex  41697  cdlemefr29exN  41725  cdleme32b  41765  cdleme32c  41766  cdleme32e  41768  cdleme35b  41773  cdleme35c  41774  cdleme35d  41775  cdleme35e  41776  cdleme35f  41777  cdleme42h  41805  cdleme42i  41806  cdleme42k  41807  cdleme48bw  41825  cdlemeg46frv  41848  cdlemeg46vrg  41850  cdlemeg46rgv  41851  cdlemeg46req  41852  cdlemf1  41884  trlord  41892  cdlemg7fvbwN  41930  cdlemg10  41964  cdlemg12e  41970  cdlemg12f  41971  cdlemg19a  42006  cdlemg31c  42022  cdlemg33c0  42025  cdlemg35  42036  tendococl  42095  cdlemh2  42139  cdlemh  42140  cdlemi  42143  cdlemk5  42159  cdlemk7  42171  cdlemk11  42172  cdlemk5u  42184  cdlemkj  42186  cdlemkuv2  42190  cdlemk7u  42193  cdlemk11u  42194  cdlemk26-3  42229  cdlemk11t  42269  cdlemk52  42277  cdlemk53a  42278  dihord1  42541  dihord2a  42542  dihord2b  42543  dihord11b  42545  dihord11c  42547  dihord2pre  42548  dihord2pre2  42549  dihord5apre  42585  dihmeetlem1N  42613  dihglblem2N  42617  dihglblem3N  42618  dihglbcpreN  42623  dihmeetlem3N  42628  dihjatc1  42634  suplesup  46624  limsupre  46924  sge0xaddlem2  47717  itscnhlc0yqe  50202  itscnhlc0xyqsol  50208  itsclquadb  50219  itsclquadeu  50220