Theorem simp31 1210

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp131  1309  simp231  1318  simp331  1327  eqfunresadj  7289  smogt  8282  frlmphl  21713  mdetuni0  22531  mdetmul  22533  gsummatr01lem3  22567  decpmatmullem  22681  tsmsxp  24065  log2sumbnd  27477  nosupres  27641  noinfres  27656  ax5seg  28911  wlkoniswlk  29633  iocinioc2  32754  totprob  34432  cgrtr  36026  cgrtr3  36028  ofscom  36041  cgrextend  36042  segconeq  36044  ifscgr  36078  btwnxfr  36090  colinearxfr  36109  brofs2  36111  brifs2  36112  fscgr  36114  btwnconn1lem1  36121  btwnconn1lem2  36122  btwnconn1lem5  36125  btwnconn1lem6  36126  btwnconn1lem7  36127  btwnconn1lem8  36128  btwnconn1lem9  36129  btwnconn1lem10  36130  btwnconn1lem11  36131  btwnconn1lem12  36132  seglecgr12im  36144  seglecgr12  36145  segletr  36148  outsideofeq  36164  ivthALT  36369  lshpkrlem5  39153  lshpkrlem6  39154  exatleN  39443  atbtwn  39485  atbtwnexOLDN  39486  atbtwnex  39487  4noncolr3  39492  3dimlem3a  39499  3dimlem4a  39502  3dim1  39506  3dim2  39507  1cvrat  39515  2atjlej  39518  hlatexch4  39520  ps-2b  39521  2atm  39566  2atmat  39600  4atlem11b  39647  4atlem11  39648  4at  39652  4at2  39653  2lplnja  39658  2lplnj  39659  dalemswapyz  39695  dalemccnedd  39726  cdlemb  39833  paddasslem5  39863  paddasslem15  39873  pmodlem1  39885  dalawlem1  39910  dalawlem3  39912  dalawlem4  39913  dalawlem5  39914  dalawlem6  39915  dalawlem7  39916  dalawlem8  39917  dalawlem9  39918  dalawlem11  39920  dalawlem12  39921  dalawlem15  39924  osumcllem5N  39999  osumcllem6N  40000  lhpexle3lem  40050  lhpmcvr4N  40065  lhpmcvr6N  40067  4atex2  40116  4atex2-0bOLDN  40118  4atex3  40120  ltrn11at  40186  trlval3  40226  cdlemd3  40239  cdleme0moN  40264  cdleme7aa  40281  cdleme7b  40283  cdleme7c  40284  cdleme7d  40285  cdleme7e  40286  cdleme7ga  40287  cdleme7  40288  cdleme16aN  40298  cdleme11dN  40301  cdleme11e  40302  cdleme11l  40308  cdleme11  40309  cdleme12  40310  cdleme14  40312  cdleme15b  40314  cdleme15c  40315  cdleme16b  40318  cdleme16c  40319  cdleme16d  40320  cdleme16e  40321  cdleme16f  40322  cdleme17c  40327  cdleme18c  40332  cdleme18d  40334  cdlemeda  40337  cdleme19a  40342  cdleme19b  40343  cdleme19c  40344  cdleme20aN  40348  cdleme20bN  40349  cdleme20d  40351  cdleme20i  40356  cdleme20j  40357  cdleme20l1  40359  cdleme20l2  40360  cdleme21d  40369  cdleme21e  40370  cdleme21f  40371  cdleme22aa  40378  cdleme22e  40383  cdleme22eALTN  40384  cdleme22f2  40386  cdleme22g  40387  cdleme23b  40389  cdleme26eALTN  40400  cdleme26fALTN  40401  cdleme26f  40402  cdleme26f2ALTN  40403  cdleme26f2  40404  cdleme28a  40409  cdleme28b  40410  cdleme32b  40481  cdleme32c  40482  cdleme32e  40484  cdleme35h  40495  cdleme35sn2aw  40497  cdleme41sn3aw  40513  cdleme41sn4aw  40514  cdlemeg46gfre  40571  cdlemf1  40600  cdlemg1cex  40627  cdlemg2ce  40631  cdlemg4d  40652  cdlemg4e  40653  cdlemg4f  40654  cdlemg4  40656  cdlemg6d  40660  cdlemg6e  40661  cdlemg7fvN  40663  cdlemg8b  40667  cdlemg8c  40668  cdlemg9a  40671  cdlemg9b  40672  cdlemg9  40673  cdlemg11aq  40677  cdlemg10a  40679  cdlemg12a  40682  cdlemg12b  40683  cdlemg12c  40684  cdlemg12d  40685  cdlemg13  40691  cdlemg14f  40692  cdlemg14g  40693  cdlemg17b  40701  cdlemg17dN  40702  cdlemg17e  40704  cdlemg17i  40708  cdlemg17pq  40711  cdlemg17iqN  40713  cdlemg18c  40719  cdlemg18d  40720  cdlemg18  40721  cdlemg19  40723  cdlemg21  40725  cdlemg27a  40731  cdlemg31b0N  40733  cdlemg27b  40735  cdlemg31c  40738  cdlemg33b0  40740  cdlemg33c0  40741  cdlemg33  40750  cdlemg35  40752  cdlemg43  40769  cdlemg44a  40770  cdlemg46  40774  cdlemh2  40855  cdlemh  40856  cdlemj1  40860  cdlemk3  40872  cdlemk5  40875  cdlemk6  40876  cdlemki  40880  cdlemksv2  40886  cdlemk12  40889  cdlemk15  40894  cdlemk16  40896  cdlemk18  40907  cdlemk19  40908  cdlemk7u  40909  cdlemk12u  40911  cdlemkoatnle-2N  40914  cdlemk13-2N  40915  cdlemkole-2N  40916  cdlemk14-2N  40917  cdlemk15-2N  40918  cdlemk16-2N  40919  cdlemk17-2N  40920  cdlemk18-2N  40925  cdlemk19-2N  40926  cdlemk7u-2N  40927  cdlemk11u-2N  40928  cdlemk12u-2N  40929  cdlemk20-2N  40931  cdlemk22  40932  cdlemk30  40933  cdlemk31  40935  cdlemk24-3  40942  cdlemkid2  40963  cdlemkfid3N  40964  cdlemk11ta  40968  cdlemkid3N  40972  cdlemk11tc  40984  cdlemk45  40986  cdlemk46  40987  cdlemk47  40988  cdlemk52  40993  cdlemk53a  40994  cdlemk53b  40995  cdleml1N  41015  cdleml3N  41017  cdlemn7  41242  cdlemn10  41245  dihordlem7  41253  dihord1  41257  dihord11c  41263  dihord2  41266  hlhilphllem  41998  fmuldfeq  45623  seposep  48957  iscnrm3rlem8  48978  iscnrm3llem2  48981