Theorem simp11r 1283

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

Assertion

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

Proof of Theorem simp11r

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  pceu  16475  maduf  21698  nllyrest  22545  exatleN  37345  2llnjaN  37507  2lplnja  37560  dalemceb  37579  pclfinN  37841  lhpexle3lem  37952  lhpmcvr5N  37968  lhpmcvr6N  37969  lhp2at0  37973  4atexlemw  37989  cdlemd2  38140  cdlemd4  38142  cdleme7aa  38183  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme7  38190  cdleme15a  38215  cdleme15b  38216  cdleme15d  38218  cdleme15  38219  cdleme16b  38220  cdleme16c  38221  cdleme16d  38222  cdleme16e  38223  cdleme16f  38224  cdleme18d  38236  cdleme19b  38245  cdleme19d  38247  cdleme19e  38248  cdleme20d  38253  cdleme20e  38254  cdleme20f  38255  cdleme20g  38256  cdleme20h  38257  cdleme20j  38259  cdleme20k  38260  cdleme20l1  38261  cdleme20l2  38262  cdleme20l  38263  cdleme20m  38264  cdleme21c  38268  cdleme21ct  38270  cdleme22cN  38283  cdleme22f  38287  cdleme22g  38289  cdleme23a  38290  cdleme23b  38291  cdleme23c  38292  cdleme25a  38294  cdleme25c  38296  cdleme25dN  38297  cdleme26ee  38301  cdleme26eALTN  38302  cdleme27N  38310  cdleme28a  38311  cdleme28b  38312  cdleme29ex  38315  cdlemefr29exN  38343  cdleme32b  38383  cdleme32c  38384  cdleme32e  38386  cdleme35b  38391  cdleme35c  38392  cdleme35d  38393  cdleme35e  38394  cdleme35f  38395  cdleme42h  38423  cdleme42i  38424  cdleme42k  38425  cdleme48bw  38443  cdlemeg46frv  38466  cdlemeg46vrg  38468  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemf1  38502  trlord  38510  cdlemg7fvbwN  38548  cdlemg10  38582  cdlemg12e  38588  cdlemg12f  38589  cdlemg19a  38624  cdlemg31c  38640  cdlemg33c0  38643  cdlemg35  38654  tendococl  38713  cdlemh2  38757  cdlemh  38758  cdlemi  38761  cdlemk5  38777  cdlemk7  38789  cdlemk11  38790  cdlemk5u  38802  cdlemkj  38804  cdlemkuv2  38808  cdlemk7u  38811  cdlemk11u  38812  cdlemk26-3  38847  cdlemk11t  38887  cdlemk52  38895  cdlemk53a  38896  dihord1  39159  dihord2a  39160  dihord2b  39161  dihord11b  39163  dihord11c  39165  dihord2pre  39166  dihord2pre2  39167  dihord5apre  39203  dihmeetlem1N  39231  dihglblem2N  39235  dihglblem3N  39236  dihglbcpreN  39241  dihmeetlem3N  39246  dihjatc1  39252  suplesup  42768  limsupre  43072  sge0xaddlem2  43862  itscnhlc0yqe  45993  itscnhlc0xyqsol  45999  itsclquadb  46010  itsclquadeu  46011