Theorem simp31 1216

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp131  1315  simp231  1324  simp331  1333  eqfunresadj  7304  smogt  8297  frlmphl  21756  mdetuni0  22604  mdetmul  22606  gsummatr01lem3  22640  decpmatmullem  22754  tsmsxp  24138  log2sumbnd  27525  nosupres  27689  noinfres  27704  ax5seg  29025  wlkoniswlk  29746  iocinioc2  32871  totprob  34611  cgrtr  36220  cgrtr3  36222  ofscom  36235  cgrextend  36236  segconeq  36238  ifscgr  36272  btwnxfr  36284  colinearxfr  36303  brofs2  36305  brifs2  36306  fscgr  36308  btwnconn1lem1  36315  btwnconn1lem2  36316  btwnconn1lem5  36319  btwnconn1lem6  36320  btwnconn1lem7  36321  btwnconn1lem8  36322  btwnconn1lem9  36323  btwnconn1lem10  36324  btwnconn1lem11  36325  btwnconn1lem12  36326  seglecgr12im  36338  seglecgr12  36339  segletr  36342  outsideofeq  36358  ivthALT  36563  lshpkrlem5  39606  lshpkrlem6  39607  exatleN  39896  atbtwn  39938  atbtwnexOLDN  39939  atbtwnex  39940  4noncolr3  39945  3dimlem3a  39952  3dimlem4a  39955  3dim1  39959  3dim2  39960  1cvrat  39968  2atjlej  39971  hlatexch4  39973  ps-2b  39974  2atm  40019  2atmat  40053  4atlem11b  40100  4atlem11  40101  4at  40105  4at2  40106  2lplnja  40111  2lplnj  40112  dalemswapyz  40148  dalemccnedd  40179  cdlemb  40286  paddasslem5  40316  paddasslem15  40326  pmodlem1  40338  dalawlem1  40363  dalawlem3  40365  dalawlem4  40366  dalawlem5  40367  dalawlem6  40368  dalawlem7  40369  dalawlem8  40370  dalawlem9  40371  dalawlem11  40373  dalawlem12  40374  dalawlem15  40377  osumcllem5N  40452  osumcllem6N  40453  lhpexle3lem  40503  lhpmcvr4N  40518  lhpmcvr6N  40520  4atex2  40569  4atex2-0bOLDN  40571  4atex3  40573  ltrn11at  40639  trlval3  40679  cdlemd3  40692  cdleme0moN  40717  cdleme7aa  40734  cdleme7b  40736  cdleme7c  40737  cdleme7d  40738  cdleme7e  40739  cdleme7ga  40740  cdleme7  40741  cdleme16aN  40751  cdleme11dN  40754  cdleme11e  40755  cdleme11l  40761  cdleme11  40762  cdleme12  40763  cdleme14  40765  cdleme15b  40767  cdleme15c  40768  cdleme16b  40771  cdleme16c  40772  cdleme16d  40773  cdleme16e  40774  cdleme16f  40775  cdleme17c  40780  cdleme18c  40785  cdleme18d  40787  cdlemeda  40790  cdleme19a  40795  cdleme19b  40796  cdleme19c  40797  cdleme20aN  40801  cdleme20bN  40802  cdleme20d  40804  cdleme20i  40809  cdleme20j  40810  cdleme20l1  40812  cdleme20l2  40813  cdleme21d  40822  cdleme21e  40823  cdleme21f  40824  cdleme22aa  40831  cdleme22e  40836  cdleme22eALTN  40837  cdleme22f2  40839  cdleme22g  40840  cdleme23b  40842  cdleme26eALTN  40853  cdleme26fALTN  40854  cdleme26f  40855  cdleme26f2ALTN  40856  cdleme26f2  40857  cdleme28a  40862  cdleme28b  40863  cdleme32b  40934  cdleme32c  40935  cdleme32e  40937  cdleme35h  40948  cdleme35sn2aw  40950  cdleme41sn3aw  40966  cdleme41sn4aw  40967  cdlemeg46gfre  41024  cdlemf1  41053  cdlemg1cex  41080  cdlemg2ce  41084  cdlemg4d  41105  cdlemg4e  41106  cdlemg4f  41107  cdlemg4  41109  cdlemg6d  41113  cdlemg6e  41114  cdlemg7fvN  41116  cdlemg8b  41120  cdlemg8c  41121  cdlemg9a  41124  cdlemg9b  41125  cdlemg9  41126  cdlemg11aq  41130  cdlemg10a  41132  cdlemg12a  41135  cdlemg12b  41136  cdlemg12c  41137  cdlemg12d  41138  cdlemg13  41144  cdlemg14f  41145  cdlemg14g  41146  cdlemg17b  41154  cdlemg17dN  41155  cdlemg17e  41157  cdlemg17i  41161  cdlemg17pq  41164  cdlemg17iqN  41166  cdlemg18c  41172  cdlemg18d  41173  cdlemg18  41174  cdlemg19  41176  cdlemg21  41178  cdlemg27a  41184  cdlemg31b0N  41186  cdlemg27b  41188  cdlemg31c  41191  cdlemg33b0  41193  cdlemg33c0  41194  cdlemg33  41203  cdlemg35  41205  cdlemg43  41222  cdlemg44a  41223  cdlemg46  41227  cdlemh2  41308  cdlemh  41309  cdlemj1  41313  cdlemk3  41325  cdlemk5  41328  cdlemk6  41329  cdlemki  41333  cdlemksv2  41339  cdlemk12  41342  cdlemk15  41347  cdlemk16  41349  cdlemk18  41360  cdlemk19  41361  cdlemk7u  41362  cdlemk12u  41364  cdlemkoatnle-2N  41367  cdlemk13-2N  41368  cdlemkole-2N  41369  cdlemk14-2N  41370  cdlemk15-2N  41371  cdlemk16-2N  41372  cdlemk17-2N  41373  cdlemk18-2N  41378  cdlemk19-2N  41379  cdlemk7u-2N  41380  cdlemk11u-2N  41381  cdlemk12u-2N  41382  cdlemk20-2N  41384  cdlemk22  41385  cdlemk30  41386  cdlemk31  41388  cdlemk24-3  41395  cdlemkid2  41416  cdlemkfid3N  41417  cdlemk11ta  41421  cdlemkid3N  41425  cdlemk11tc  41437  cdlemk45  41439  cdlemk46  41440  cdlemk47  41441  cdlemk52  41446  cdlemk53a  41447  cdlemk53b  41448  cdleml1N  41468  cdleml3N  41470  cdlemn7  41695  cdlemn10  41698  dihordlem7  41706  dihord1  41710  dihord11c  41716  dihord2  41719  hlhilphllem  42451  fmuldfeq  46028  seposep  49416  iscnrm3rlem8  49437  iscnrm3llem2  49440