Theorem simp31 1205

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 1132	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜒)
2	1	3ad2ant3 1131	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ 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:  simp131  1304  simp231  1313  simp331  1322  smogt  8004  frlmphl  20925  mdetuni0  21230  mdetmul  21232  gsummatr01lem3  21266  decpmatmullem  21379  tsmsxp  22763  log2sumbnd  26120  ax5seg  26724  wlkoniswlk  27443  iocinioc2  30502  totprob  31685  eqfunresadj  33004  nosupres  33207  cgrtr  33453  cgrtr3  33455  ofscom  33468  cgrextend  33469  segconeq  33471  ifscgr  33505  btwnxfr  33517  colinearxfr  33536  brofs2  33538  brifs2  33539  fscgr  33541  btwnconn1lem1  33548  btwnconn1lem2  33549  btwnconn1lem5  33552  btwnconn1lem6  33553  btwnconn1lem7  33554  btwnconn1lem8  33555  btwnconn1lem9  33556  btwnconn1lem10  33557  btwnconn1lem11  33558  btwnconn1lem12  33559  seglecgr12im  33571  seglecgr12  33572  segletr  33575  outsideofeq  33591  ivthALT  33683  lshpkrlem5  36265  lshpkrlem6  36266  exatleN  36555  atbtwn  36597  atbtwnexOLDN  36598  atbtwnex  36599  4noncolr3  36604  3dimlem3a  36611  3dimlem4a  36614  3dim1  36618  3dim2  36619  1cvrat  36627  2atjlej  36630  hlatexch4  36632  ps-2b  36633  2atm  36678  2atmat  36712  4atlem11b  36759  4atlem11  36760  4at  36764  4at2  36765  2lplnja  36770  2lplnj  36771  dalemswapyz  36807  dalemccnedd  36838  cdlemb  36945  paddasslem5  36975  paddasslem15  36985  pmodlem1  36997  dalawlem1  37022  dalawlem3  37024  dalawlem4  37025  dalawlem5  37026  dalawlem6  37027  dalawlem7  37028  dalawlem8  37029  dalawlem9  37030  dalawlem11  37032  dalawlem12  37033  dalawlem15  37036  osumcllem5N  37111  osumcllem6N  37112  lhpexle3lem  37162  lhpmcvr4N  37177  lhpmcvr6N  37179  4atex2  37228  4atex2-0bOLDN  37230  4atex3  37232  ltrn11at  37298  trlval3  37338  cdlemd3  37351  cdleme0moN  37376  cdleme7aa  37393  cdleme7b  37395  cdleme7c  37396  cdleme7d  37397  cdleme7e  37398  cdleme7ga  37399  cdleme7  37400  cdleme16aN  37410  cdleme11dN  37413  cdleme11e  37414  cdleme11l  37420  cdleme11  37421  cdleme12  37422  cdleme14  37424  cdleme15b  37426  cdleme15c  37427  cdleme16b  37430  cdleme16c  37431  cdleme16d  37432  cdleme16e  37433  cdleme16f  37434  cdleme17c  37439  cdleme18c  37444  cdleme18d  37446  cdlemeda  37449  cdleme19a  37454  cdleme19b  37455  cdleme19c  37456  cdleme20aN  37460  cdleme20bN  37461  cdleme20d  37463  cdleme20i  37468  cdleme20j  37469  cdleme20l1  37471  cdleme20l2  37472  cdleme21d  37481  cdleme21e  37482  cdleme21f  37483  cdleme22aa  37490  cdleme22e  37495  cdleme22eALTN  37496  cdleme22f2  37498  cdleme22g  37499  cdleme23b  37501  cdleme26eALTN  37512  cdleme26fALTN  37513  cdleme26f  37514  cdleme26f2ALTN  37515  cdleme26f2  37516  cdleme28a  37521  cdleme28b  37522  cdleme32b  37593  cdleme32c  37594  cdleme32e  37596  cdleme35h  37607  cdleme35sn2aw  37609  cdleme41sn3aw  37625  cdleme41sn4aw  37626  cdlemeg46gfre  37683  cdlemf1  37712  cdlemg1cex  37739  cdlemg2ce  37743  cdlemg4d  37764  cdlemg4e  37765  cdlemg4f  37766  cdlemg4  37768  cdlemg6d  37772  cdlemg6e  37773  cdlemg7fvN  37775  cdlemg8b  37779  cdlemg8c  37780  cdlemg9a  37783  cdlemg9b  37784  cdlemg9  37785  cdlemg11aq  37789  cdlemg10a  37791  cdlemg12a  37794  cdlemg12b  37795  cdlemg12c  37796  cdlemg12d  37797  cdlemg13  37803  cdlemg14f  37804  cdlemg14g  37805  cdlemg17b  37813  cdlemg17dN  37814  cdlemg17e  37816  cdlemg17i  37820  cdlemg17pq  37823  cdlemg17iqN  37825  cdlemg18c  37831  cdlemg18d  37832  cdlemg18  37833  cdlemg19  37835  cdlemg21  37837  cdlemg27a  37843  cdlemg31b0N  37845  cdlemg27b  37847  cdlemg31c  37850  cdlemg33b0  37852  cdlemg33c0  37853  cdlemg33  37862  cdlemg35  37864  cdlemg43  37881  cdlemg44a  37882  cdlemg46  37886  cdlemh2  37967  cdlemh  37968  cdlemj1  37972  cdlemk3  37984  cdlemk5  37987  cdlemk6  37988  cdlemki  37992  cdlemksv2  37998  cdlemk12  38001  cdlemk15  38006  cdlemk16  38008  cdlemk18  38019  cdlemk19  38020  cdlemk7u  38021  cdlemk12u  38023  cdlemkoatnle-2N  38026  cdlemk13-2N  38027  cdlemkole-2N  38028  cdlemk14-2N  38029  cdlemk15-2N  38030  cdlemk16-2N  38031  cdlemk17-2N  38032  cdlemk18-2N  38037  cdlemk19-2N  38038  cdlemk7u-2N  38039  cdlemk11u-2N  38040  cdlemk12u-2N  38041  cdlemk20-2N  38043  cdlemk22  38044  cdlemk30  38045  cdlemk31  38047  cdlemk24-3  38054  cdlemkid2  38075  cdlemkfid3N  38076  cdlemk11ta  38080  cdlemkid3N  38084  cdlemk11tc  38096  cdlemk45  38098  cdlemk46  38099  cdlemk47  38100  cdlemk52  38105  cdlemk53a  38106  cdlemk53b  38107  cdleml1N  38127  cdleml3N  38129  cdlemn7  38354  cdlemn10  38357  dihordlem7  38365  dihord1  38369  dihord11c  38375  dihord2  38378  hlhilphllem  39110  fmuldfeq  41884