Theorem simp31 1228

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp131  1327  simp231  1336  simp331  1345  eqfunresadj  7401  smogt  8413  frlmphl  22142  mdetuni0  22991  mdetmul  22993  gsummatr01lem3  23027  decpmatmullem  23144  tsmsxp  24529  log2sumbnd  27928  nosupres  28121  noinfres  28136  ax5seg  29573  wlkoniswlk  30297  iocinioc2  33467  totprob  35170  cgrtr  36972  cgrtr3  36974  ofscom  36987  cgrextend  36988  segconeq  36990  ifscgr  37024  btwnxfr  37036  colinearxfr  37055  brofs2  37057  brifs2  37058  fscgr  37060  btwnconn1lem1  37067  btwnconn1lem2  37068  btwnconn1lem5  37071  btwnconn1lem6  37072  btwnconn1lem7  37073  btwnconn1lem8  37074  btwnconn1lem9  37075  btwnconn1lem10  37076  btwnconn1lem11  37077  btwnconn1lem12  37078  seglecgr12im  37090  seglecgr12  37091  segletr  37094  outsideofeq  37110  ivthALT  37338  lshpkrlem5  40437  lshpkrlem6  40438  exatleN  40727  atbtwn  40769  atbtwnexOLDN  40770  atbtwnex  40771  4noncolr3  40776  3dimlem3a  40783  3dimlem4a  40786  3dim1  40790  3dim2  40791  1cvrat  40799  2atjlej  40802  hlatexch4  40804  ps-2b  40805  2atm  40850  2atmat  40884  4atlem11b  40931  4atlem11  40932  4at  40936  4at2  40937  2lplnja  40942  2lplnj  40943  dalemswapyz  40979  dalemccnedd  41010  cdlemb  41117  paddasslem5  41147  paddasslem15  41157  pmodlem1  41169  dalawlem1  41194  dalawlem3  41196  dalawlem4  41197  dalawlem5  41198  dalawlem6  41199  dalawlem7  41200  dalawlem8  41201  dalawlem9  41202  dalawlem11  41204  dalawlem12  41205  dalawlem15  41208  osumcllem5N  41283  osumcllem6N  41284  lhpexle3lem  41334  lhpmcvr4N  41349  lhpmcvr6N  41351  4atex2  41400  4atex2-0bOLDN  41402  4atex3  41404  ltrn11at  41470  trlval3  41510  cdlemd3  41523  cdleme0moN  41548  cdleme7aa  41565  cdleme7b  41567  cdleme7c  41568  cdleme7d  41569  cdleme7e  41570  cdleme7ga  41571  cdleme7  41572  cdleme16aN  41582  cdleme11dN  41585  cdleme11e  41586  cdleme11l  41592  cdleme11  41593  cdleme12  41594  cdleme14  41596  cdleme15b  41598  cdleme15c  41599  cdleme16b  41602  cdleme16c  41603  cdleme16d  41604  cdleme16e  41605  cdleme16f  41606  cdleme17c  41611  cdleme18c  41616  cdleme18d  41618  cdlemeda  41621  cdleme19a  41626  cdleme19b  41627  cdleme19c  41628  cdleme20aN  41632  cdleme20bN  41633  cdleme20d  41635  cdleme20i  41640  cdleme20j  41641  cdleme20l1  41643  cdleme20l2  41644  cdleme21d  41653  cdleme21e  41654  cdleme21f  41655  cdleme22aa  41662  cdleme22e  41667  cdleme22eALTN  41668  cdleme22f2  41670  cdleme22g  41671  cdleme23b  41673  cdleme26eALTN  41684  cdleme26fALTN  41685  cdleme26f  41686  cdleme26f2ALTN  41687  cdleme26f2  41688  cdleme28a  41693  cdleme28b  41694  cdleme32b  41765  cdleme32c  41766  cdleme32e  41768  cdleme35h  41779  cdleme35sn2aw  41781  cdleme41sn3aw  41797  cdleme41sn4aw  41798  cdlemeg46gfre  41855  cdlemf1  41884  cdlemg1cex  41911  cdlemg2ce  41915  cdlemg4d  41936  cdlemg4e  41937  cdlemg4f  41938  cdlemg4  41940  cdlemg6d  41944  cdlemg6e  41945  cdlemg7fvN  41947  cdlemg8b  41951  cdlemg8c  41952  cdlemg9a  41955  cdlemg9b  41956  cdlemg9  41957  cdlemg11aq  41961  cdlemg10a  41963  cdlemg12a  41966  cdlemg12b  41967  cdlemg12c  41968  cdlemg12d  41969  cdlemg13  41975  cdlemg14f  41976  cdlemg14g  41977  cdlemg17b  41985  cdlemg17dN  41986  cdlemg17e  41988  cdlemg17i  41992  cdlemg17pq  41995  cdlemg17iqN  41997  cdlemg18c  42003  cdlemg18d  42004  cdlemg18  42005  cdlemg19  42007  cdlemg21  42009  cdlemg27a  42015  cdlemg31b0N  42017  cdlemg27b  42019  cdlemg31c  42022  cdlemg33b0  42024  cdlemg33c0  42025  cdlemg33  42034  cdlemg35  42036  cdlemg43  42053  cdlemg44a  42054  cdlemg46  42058  cdlemh2  42139  cdlemh  42140  cdlemj1  42144  cdlemk3  42156  cdlemk5  42159  cdlemk6  42160  cdlemki  42164  cdlemksv2  42170  cdlemk12  42173  cdlemk15  42178  cdlemk16  42180  cdlemk18  42191  cdlemk19  42192  cdlemk7u  42193  cdlemk12u  42195  cdlemkoatnle-2N  42198  cdlemk13-2N  42199  cdlemkole-2N  42200  cdlemk14-2N  42201  cdlemk15-2N  42202  cdlemk16-2N  42203  cdlemk17-2N  42204  cdlemk18-2N  42209  cdlemk19-2N  42210  cdlemk7u-2N  42211  cdlemk11u-2N  42212  cdlemk12u-2N  42213  cdlemk20-2N  42215  cdlemk22  42216  cdlemk30  42217  cdlemk31  42219  cdlemk24-3  42226  cdlemkid2  42247  cdlemkfid3N  42248  cdlemk11ta  42252  cdlemkid3N  42256  cdlemk11tc  42268  cdlemk45  42270  cdlemk46  42271  cdlemk47  42272  cdlemk52  42277  cdlemk53a  42278  cdlemk53b  42279  cdleml1N  42299  cdleml3N  42301  cdlemn7  42526  cdlemn10  42529  dihordlem7  42537  dihord1  42541  dihord11c  42547  dihord2  42550  hlhilphllem  43282  fmuldfeq  46868  seposep  50371  iscnrm3rlem8  50392  iscnrm3llem2  50395