Theorem simp31 1097

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

Syntax hints:   → wi 4   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simpl31  1142  simpr31  1151  simp131  1196  simp231  1205  simp331  1214  smogt  7464  frlmphl  20120  mdetuni0  20427  mdetmul  20429  gsummatr01lem3  20463  decpmatmullem  20576  tsmsxp  21958  log2sumbnd  25233  ax5seg  25818  wlkoniswlk  26557  iocinioc2  29541  totprob  30489  eqfunresadj  31659  nosupres  31853  cgrtr  32099  cgrtr3  32101  ofscom  32114  cgrextend  32115  segconeq  32117  ifscgr  32151  btwnxfr  32163  colinearxfr  32182  brofs2  32184  brifs2  32185  fscgr  32187  btwnconn1lem1  32194  btwnconn1lem2  32195  btwnconn1lem5  32198  btwnconn1lem6  32199  btwnconn1lem7  32200  btwnconn1lem8  32201  btwnconn1lem9  32202  btwnconn1lem10  32203  btwnconn1lem11  32204  btwnconn1lem12  32205  seglecgr12im  32217  seglecgr12  32218  segletr  32221  outsideofeq  32237  ivthALT  32330  lshpkrlem5  34401  lshpkrlem6  34402  exatleN  34690  atbtwn  34732  atbtwnexOLDN  34733  atbtwnex  34734  4noncolr3  34739  3dimlem3a  34746  3dimlem4a  34749  3dim1  34753  3dim2  34754  1cvrat  34762  2atjlej  34765  hlatexch4  34767  ps-2b  34768  2atm  34813  2atmat  34847  4atlem11b  34894  4atlem11  34895  4at  34899  4at2  34900  2lplnja  34905  2lplnj  34906  dalemswapyz  34942  dalemccnedd  34973  cdlemb  35080  paddasslem5  35110  paddasslem15  35120  pmodlem1  35132  dalawlem1  35157  dalawlem3  35159  dalawlem4  35160  dalawlem5  35161  dalawlem6  35162  dalawlem7  35163  dalawlem8  35164  dalawlem9  35165  dalawlem11  35167  dalawlem12  35168  dalawlem15  35171  osumcllem5N  35246  osumcllem6N  35247  lhpexle3lem  35297  lhpmcvr4N  35312  lhpmcvr6N  35314  4atex2  35363  4atex2-0bOLDN  35365  4atex3  35367  ltrn11at  35433  trlval3  35474  cdlemd3  35487  cdleme0moN  35512  cdleme7aa  35529  cdleme7b  35531  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme16aN  35546  cdleme11dN  35549  cdleme11e  35550  cdleme11l  35556  cdleme11  35557  cdleme12  35558  cdleme14  35560  cdleme15b  35562  cdleme15c  35563  cdleme16b  35566  cdleme16c  35567  cdleme16d  35568  cdleme16e  35569  cdleme16f  35570  cdleme17c  35575  cdleme18c  35580  cdleme18d  35582  cdlemeda  35585  cdleme19a  35591  cdleme19b  35592  cdleme19c  35593  cdleme20aN  35597  cdleme20bN  35598  cdleme20d  35600  cdleme20i  35605  cdleme20j  35606  cdleme20l1  35608  cdleme20l2  35609  cdleme21d  35618  cdleme21e  35619  cdleme21f  35620  cdleme22aa  35627  cdleme22e  35632  cdleme22eALTN  35633  cdleme22f2  35635  cdleme22g  35636  cdleme23b  35638  cdleme26eALTN  35649  cdleme26fALTN  35650  cdleme26f  35651  cdleme26f2ALTN  35652  cdleme26f2  35653  cdleme28a  35658  cdleme28b  35659  cdleme32b  35730  cdleme32c  35731  cdleme32e  35733  cdleme35h  35744  cdleme35sn2aw  35746  cdleme41sn3aw  35762  cdleme41sn4aw  35763  cdlemeg46gfre  35820  cdlemf1  35849  cdlemg1cex  35876  cdlemg2ce  35880  cdlemg4d  35901  cdlemg4e  35902  cdlemg4f  35903  cdlemg4  35905  cdlemg6d  35909  cdlemg6e  35910  cdlemg7fvN  35912  cdlemg8b  35916  cdlemg8c  35917  cdlemg9a  35920  cdlemg9b  35921  cdlemg9  35922  cdlemg11aq  35926  cdlemg10a  35928  cdlemg12a  35931  cdlemg12b  35932  cdlemg12c  35933  cdlemg12d  35934  cdlemg13  35940  cdlemg14f  35941  cdlemg14g  35942  cdlemg17b  35950  cdlemg17dN  35951  cdlemg17e  35953  cdlemg17i  35957  cdlemg17pq  35960  cdlemg17iqN  35962  cdlemg18c  35968  cdlemg18d  35969  cdlemg18  35970  cdlemg19  35972  cdlemg21  35974  cdlemg27a  35980  cdlemg31b0N  35982  cdlemg27b  35984  cdlemg31c  35987  cdlemg33b0  35989  cdlemg33c0  35990  cdlemg33  35999  cdlemg35  36001  cdlemg43  36018  cdlemg44a  36019  cdlemg46  36023  cdlemh2  36104  cdlemh  36105  cdlemj1  36109  cdlemk3  36121  cdlemk5  36124  cdlemk6  36125  cdlemki  36129  cdlemksv2  36135  cdlemk12  36138  cdlemk15  36143  cdlemk16  36145  cdlemk18  36156  cdlemk19  36157  cdlemk7u  36158  cdlemk12u  36160  cdlemkoatnle-2N  36163  cdlemk13-2N  36164  cdlemkole-2N  36165  cdlemk14-2N  36166  cdlemk15-2N  36167  cdlemk16-2N  36168  cdlemk17-2N  36169  cdlemk18-2N  36174  cdlemk19-2N  36175  cdlemk7u-2N  36176  cdlemk11u-2N  36177  cdlemk12u-2N  36178  cdlemk20-2N  36180  cdlemk22  36181  cdlemk30  36182  cdlemk31  36184  cdlemk24-3  36191  cdlemkid2  36212  cdlemkfid3N  36213  cdlemk11ta  36217  cdlemkid3N  36221  cdlemk11tc  36233  cdlemk45  36235  cdlemk46  36236  cdlemk47  36237  cdlemk52  36242  cdlemk53a  36243  cdlemk53b  36244  cdleml1N  36264  cdleml3N  36266  cdlemn7  36492  cdlemn10  36495  dihordlem7  36503  dihord1  36507  dihord11c  36513  dihord2  36516  hlhilphllem  37251  fmuldfeq  39815