Theorem simp11r 1281

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

Assertion

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

Proof of Theorem simp11r

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  pceu  16177  maduf  21244  nllyrest  22088  exatleN  36534  2llnjaN  36696  2lplnja  36749  dalemceb  36768  pclfinN  37030  lhpexle3lem  37141  lhpmcvr5N  37157  lhpmcvr6N  37158  lhp2at0  37162  4atexlemw  37178  cdlemd2  37329  cdlemd4  37331  cdleme7aa  37372  cdleme7c  37375  cdleme7d  37376  cdleme7e  37377  cdleme7ga  37378  cdleme7  37379  cdleme15a  37404  cdleme15b  37405  cdleme15d  37407  cdleme15  37408  cdleme16b  37409  cdleme16c  37410  cdleme16d  37411  cdleme16e  37412  cdleme16f  37413  cdleme18d  37425  cdleme19b  37434  cdleme19d  37436  cdleme19e  37437  cdleme20d  37442  cdleme20e  37443  cdleme20f  37444  cdleme20g  37445  cdleme20h  37446  cdleme20j  37448  cdleme20k  37449  cdleme20l1  37450  cdleme20l2  37451  cdleme20l  37452  cdleme20m  37453  cdleme21c  37457  cdleme21ct  37459  cdleme22cN  37472  cdleme22f  37476  cdleme22g  37478  cdleme23a  37479  cdleme23b  37480  cdleme23c  37481  cdleme25a  37483  cdleme25c  37485  cdleme25dN  37486  cdleme26ee  37490  cdleme26eALTN  37491  cdleme27N  37499  cdleme28a  37500  cdleme28b  37501  cdleme29ex  37504  cdlemefr29exN  37532  cdleme32b  37572  cdleme32c  37573  cdleme32e  37575  cdleme35b  37580  cdleme35c  37581  cdleme35d  37582  cdleme35e  37583  cdleme35f  37584  cdleme42h  37612  cdleme42i  37613  cdleme42k  37614  cdleme48bw  37632  cdlemeg46frv  37655  cdlemeg46vrg  37657  cdlemeg46rgv  37658  cdlemeg46req  37659  cdlemf1  37691  trlord  37699  cdlemg7fvbwN  37737  cdlemg10  37771  cdlemg12e  37777  cdlemg12f  37778  cdlemg19a  37813  cdlemg31c  37829  cdlemg33c0  37832  cdlemg35  37843  tendococl  37902  cdlemh2  37946  cdlemh  37947  cdlemi  37950  cdlemk5  37966  cdlemk7  37978  cdlemk11  37979  cdlemk5u  37991  cdlemkj  37993  cdlemkuv2  37997  cdlemk7u  38000  cdlemk11u  38001  cdlemk26-3  38036  cdlemk11t  38076  cdlemk52  38084  cdlemk53a  38085  dihord1  38348  dihord2a  38349  dihord2b  38350  dihord11b  38352  dihord11c  38354  dihord2pre  38355  dihord2pre2  38356  dihord5apre  38392  dihmeetlem1N  38420  dihglblem2N  38424  dihglblem3N  38425  dihglbcpreN  38430  dihmeetlem3N  38435  dihjatc1  38441  suplesup  41599  limsupre  41914  sge0xaddlem2  42709  itscnhlc0yqe  44739  itscnhlc0xyqsol  44745  itsclquadb  44756  itsclquadeu  44757