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 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  16884  maduf  22647  nllyrest  23494  exatleN  39406  2llnjaN  39568  2lplnja  39621  dalemceb  39640  pclfinN  39902  lhpexle3lem  40013  lhpmcvr5N  40029  lhpmcvr6N  40030  lhp2at0  40034  4atexlemw  40050  cdlemd2  40201  cdlemd4  40203  cdleme7aa  40244  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme7  40251  cdleme15a  40276  cdleme15b  40277  cdleme15d  40279  cdleme15  40280  cdleme16b  40281  cdleme16c  40282  cdleme16d  40283  cdleme16e  40284  cdleme16f  40285  cdleme18d  40297  cdleme19b  40306  cdleme19d  40308  cdleme19e  40309  cdleme20d  40314  cdleme20e  40315  cdleme20f  40316  cdleme20g  40317  cdleme20h  40318  cdleme20j  40320  cdleme20k  40321  cdleme20l1  40322  cdleme20l2  40323  cdleme20l  40324  cdleme20m  40325  cdleme21c  40329  cdleme21ct  40331  cdleme22cN  40344  cdleme22f  40348  cdleme22g  40350  cdleme23a  40351  cdleme23b  40352  cdleme23c  40353  cdleme25a  40355  cdleme25c  40357  cdleme25dN  40358  cdleme26ee  40362  cdleme26eALTN  40363  cdleme27N  40371  cdleme28a  40372  cdleme28b  40373  cdleme29ex  40376  cdlemefr29exN  40404  cdleme32b  40444  cdleme32c  40445  cdleme32e  40447  cdleme35b  40452  cdleme35c  40453  cdleme35d  40454  cdleme35e  40455  cdleme35f  40456  cdleme42h  40484  cdleme42i  40485  cdleme42k  40486  cdleme48bw  40504  cdlemeg46frv  40527  cdlemeg46vrg  40529  cdlemeg46rgv  40530  cdlemeg46req  40531  cdlemf1  40563  trlord  40571  cdlemg7fvbwN  40609  cdlemg10  40643  cdlemg12e  40649  cdlemg12f  40650  cdlemg19a  40685  cdlemg31c  40701  cdlemg33c0  40704  cdlemg35  40715  tendococl  40774  cdlemh2  40818  cdlemh  40819  cdlemi  40822  cdlemk5  40838  cdlemk7  40850  cdlemk11  40851  cdlemk5u  40863  cdlemkj  40865  cdlemkuv2  40869  cdlemk7u  40872  cdlemk11u  40873  cdlemk26-3  40908  cdlemk11t  40948  cdlemk52  40956  cdlemk53a  40957  dihord1  41220  dihord2a  41221  dihord2b  41222  dihord11b  41224  dihord11c  41226  dihord2pre  41227  dihord2pre2  41228  dihord5apre  41264  dihmeetlem1N  41292  dihglblem2N  41296  dihglblem3N  41297  dihglbcpreN  41302  dihmeetlem3N  41307  dihjatc1  41313  suplesup  45350  limsupre  45656  sge0xaddlem2  46449  itscnhlc0yqe  48680  itscnhlc0xyqsol  48686  itsclquadb  48697  itsclquadeu  48698