Theorem simp31 1207

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

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

Proof of Theorem simp31

Step	Hyp	Ref	Expression
1		simp1 1134	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜒)
2	1	3ad2ant3 1133	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ 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:  simp131  1306  simp231  1315  simp331  1324  eqfunresadj  7362  smogt  8381  frlmphl  21708  mdetuni0  22516  mdetmul  22518  gsummatr01lem3  22552  decpmatmullem  22666  tsmsxp  24052  log2sumbnd  27470  nosupres  27633  noinfres  27648  ax5seg  28742  wlkoniswlk  29468  iocinioc2  32541  totprob  34041  cgrtr  35582  cgrtr3  35584  ofscom  35597  cgrextend  35598  segconeq  35600  ifscgr  35634  btwnxfr  35646  colinearxfr  35665  brofs2  35667  brifs2  35668  fscgr  35670  btwnconn1lem1  35677  btwnconn1lem2  35678  btwnconn1lem5  35681  btwnconn1lem6  35682  btwnconn1lem7  35683  btwnconn1lem8  35684  btwnconn1lem9  35685  btwnconn1lem10  35686  btwnconn1lem11  35687  btwnconn1lem12  35688  seglecgr12im  35700  seglecgr12  35701  segletr  35704  outsideofeq  35720  ivthALT  35813  lshpkrlem5  38580  lshpkrlem6  38581  exatleN  38871  atbtwn  38913  atbtwnexOLDN  38914  atbtwnex  38915  4noncolr3  38920  3dimlem3a  38927  3dimlem4a  38930  3dim1  38934  3dim2  38935  1cvrat  38943  2atjlej  38946  hlatexch4  38948  ps-2b  38949  2atm  38994  2atmat  39028  4atlem11b  39075  4atlem11  39076  4at  39080  4at2  39081  2lplnja  39086  2lplnj  39087  dalemswapyz  39123  dalemccnedd  39154  cdlemb  39261  paddasslem5  39291  paddasslem15  39301  pmodlem1  39313  dalawlem1  39338  dalawlem3  39340  dalawlem4  39341  dalawlem5  39342  dalawlem6  39343  dalawlem7  39344  dalawlem8  39345  dalawlem9  39346  dalawlem11  39348  dalawlem12  39349  dalawlem15  39352  osumcllem5N  39427  osumcllem6N  39428  lhpexle3lem  39478  lhpmcvr4N  39493  lhpmcvr6N  39495  4atex2  39544  4atex2-0bOLDN  39546  4atex3  39548  ltrn11at  39614  trlval3  39654  cdlemd3  39667  cdleme0moN  39692  cdleme7aa  39709  cdleme7b  39711  cdleme7c  39712  cdleme7d  39713  cdleme7e  39714  cdleme7ga  39715  cdleme7  39716  cdleme16aN  39726  cdleme11dN  39729  cdleme11e  39730  cdleme11l  39736  cdleme11  39737  cdleme12  39738  cdleme14  39740  cdleme15b  39742  cdleme15c  39743  cdleme16b  39746  cdleme16c  39747  cdleme16d  39748  cdleme16e  39749  cdleme16f  39750  cdleme17c  39755  cdleme18c  39760  cdleme18d  39762  cdlemeda  39765  cdleme19a  39770  cdleme19b  39771  cdleme19c  39772  cdleme20aN  39776  cdleme20bN  39777  cdleme20d  39779  cdleme20i  39784  cdleme20j  39785  cdleme20l1  39787  cdleme20l2  39788  cdleme21d  39797  cdleme21e  39798  cdleme21f  39799  cdleme22aa  39806  cdleme22e  39811  cdleme22eALTN  39812  cdleme22f2  39814  cdleme22g  39815  cdleme23b  39817  cdleme26eALTN  39828  cdleme26fALTN  39829  cdleme26f  39830  cdleme26f2ALTN  39831  cdleme26f2  39832  cdleme28a  39837  cdleme28b  39838  cdleme32b  39909  cdleme32c  39910  cdleme32e  39912  cdleme35h  39923  cdleme35sn2aw  39925  cdleme41sn3aw  39941  cdleme41sn4aw  39942  cdlemeg46gfre  39999  cdlemf1  40028  cdlemg1cex  40055  cdlemg2ce  40059  cdlemg4d  40080  cdlemg4e  40081  cdlemg4f  40082  cdlemg4  40084  cdlemg6d  40088  cdlemg6e  40089  cdlemg7fvN  40091  cdlemg8b  40095  cdlemg8c  40096  cdlemg9a  40099  cdlemg9b  40100  cdlemg9  40101  cdlemg11aq  40105  cdlemg10a  40107  cdlemg12a  40110  cdlemg12b  40111  cdlemg12c  40112  cdlemg12d  40113  cdlemg13  40119  cdlemg14f  40120  cdlemg14g  40121  cdlemg17b  40129  cdlemg17dN  40130  cdlemg17e  40132  cdlemg17i  40136  cdlemg17pq  40139  cdlemg17iqN  40141  cdlemg18c  40147  cdlemg18d  40148  cdlemg18  40149  cdlemg19  40151  cdlemg21  40153  cdlemg27a  40159  cdlemg31b0N  40161  cdlemg27b  40163  cdlemg31c  40166  cdlemg33b0  40168  cdlemg33c0  40169  cdlemg33  40178  cdlemg35  40180  cdlemg43  40197  cdlemg44a  40198  cdlemg46  40202  cdlemh2  40283  cdlemh  40284  cdlemj1  40288  cdlemk3  40300  cdlemk5  40303  cdlemk6  40304  cdlemki  40308  cdlemksv2  40314  cdlemk12  40317  cdlemk15  40322  cdlemk16  40324  cdlemk18  40335  cdlemk19  40336  cdlemk7u  40337  cdlemk12u  40339  cdlemkoatnle-2N  40342  cdlemk13-2N  40343  cdlemkole-2N  40344  cdlemk14-2N  40345  cdlemk15-2N  40346  cdlemk16-2N  40347  cdlemk17-2N  40348  cdlemk18-2N  40353  cdlemk19-2N  40354  cdlemk7u-2N  40355  cdlemk11u-2N  40356  cdlemk12u-2N  40357  cdlemk20-2N  40359  cdlemk22  40360  cdlemk30  40361  cdlemk31  40363  cdlemk24-3  40370  cdlemkid2  40391  cdlemkfid3N  40392  cdlemk11ta  40396  cdlemkid3N  40400  cdlemk11tc  40412  cdlemk45  40414  cdlemk46  40415  cdlemk47  40416  cdlemk52  40421  cdlemk53a  40422  cdlemk53b  40423  cdleml1N  40443  cdleml3N  40445  cdlemn7  40670  cdlemn10  40673  dihordlem7  40681  dihord1  40685  dihord11c  40691  dihord2  40694  hlhilphllem  41430  fmuldfeq  44965  seposep  47938  iscnrm3rlem8  47960  iscnrm3llem2  47963

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »