Theorem simp31 1208

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 1135	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜒)
2	1	3ad2ant3 1134	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  1307  simp231  1316  simp331  1325  eqfunresadj  7379  smogt  8405  frlmphl  21818  mdetuni0  22642  mdetmul  22644  gsummatr01lem3  22678  decpmatmullem  22792  tsmsxp  24178  log2sumbnd  27602  nosupres  27766  noinfres  27781  ax5seg  28967  wlkoniswlk  29693  iocinioc2  32787  totprob  34408  cgrtr  35973  cgrtr3  35975  ofscom  35988  cgrextend  35989  segconeq  35991  ifscgr  36025  btwnxfr  36037  colinearxfr  36056  brofs2  36058  brifs2  36059  fscgr  36061  btwnconn1lem1  36068  btwnconn1lem2  36069  btwnconn1lem5  36072  btwnconn1lem6  36073  btwnconn1lem7  36074  btwnconn1lem8  36075  btwnconn1lem9  36076  btwnconn1lem10  36077  btwnconn1lem11  36078  btwnconn1lem12  36079  seglecgr12im  36091  seglecgr12  36092  segletr  36095  outsideofeq  36111  ivthALT  36317  lshpkrlem5  39095  lshpkrlem6  39096  exatleN  39386  atbtwn  39428  atbtwnexOLDN  39429  atbtwnex  39430  4noncolr3  39435  3dimlem3a  39442  3dimlem4a  39445  3dim1  39449  3dim2  39450  1cvrat  39458  2atjlej  39461  hlatexch4  39463  ps-2b  39464  2atm  39509  2atmat  39543  4atlem11b  39590  4atlem11  39591  4at  39595  4at2  39596  2lplnja  39601  2lplnj  39602  dalemswapyz  39638  dalemccnedd  39669  cdlemb  39776  paddasslem5  39806  paddasslem15  39816  pmodlem1  39828  dalawlem1  39853  dalawlem3  39855  dalawlem4  39856  dalawlem5  39857  dalawlem6  39858  dalawlem7  39859  dalawlem8  39860  dalawlem9  39861  dalawlem11  39863  dalawlem12  39864  dalawlem15  39867  osumcllem5N  39942  osumcllem6N  39943  lhpexle3lem  39993  lhpmcvr4N  40008  lhpmcvr6N  40010  4atex2  40059  4atex2-0bOLDN  40061  4atex3  40063  ltrn11at  40129  trlval3  40169  cdlemd3  40182  cdleme0moN  40207  cdleme7aa  40224  cdleme7b  40226  cdleme7c  40227  cdleme7d  40228  cdleme7e  40229  cdleme7ga  40230  cdleme7  40231  cdleme16aN  40241  cdleme11dN  40244  cdleme11e  40245  cdleme11l  40251  cdleme11  40252  cdleme12  40253  cdleme14  40255  cdleme15b  40257  cdleme15c  40258  cdleme16b  40261  cdleme16c  40262  cdleme16d  40263  cdleme16e  40264  cdleme16f  40265  cdleme17c  40270  cdleme18c  40275  cdleme18d  40277  cdlemeda  40280  cdleme19a  40285  cdleme19b  40286  cdleme19c  40287  cdleme20aN  40291  cdleme20bN  40292  cdleme20d  40294  cdleme20i  40299  cdleme20j  40300  cdleme20l1  40302  cdleme20l2  40303  cdleme21d  40312  cdleme21e  40313  cdleme21f  40314  cdleme22aa  40321  cdleme22e  40326  cdleme22eALTN  40327  cdleme22f2  40329  cdleme22g  40330  cdleme23b  40332  cdleme26eALTN  40343  cdleme26fALTN  40344  cdleme26f  40345  cdleme26f2ALTN  40346  cdleme26f2  40347  cdleme28a  40352  cdleme28b  40353  cdleme32b  40424  cdleme32c  40425  cdleme32e  40427  cdleme35h  40438  cdleme35sn2aw  40440  cdleme41sn3aw  40456  cdleme41sn4aw  40457  cdlemeg46gfre  40514  cdlemf1  40543  cdlemg1cex  40570  cdlemg2ce  40574  cdlemg4d  40595  cdlemg4e  40596  cdlemg4f  40597  cdlemg4  40599  cdlemg6d  40603  cdlemg6e  40604  cdlemg7fvN  40606  cdlemg8b  40610  cdlemg8c  40611  cdlemg9a  40614  cdlemg9b  40615  cdlemg9  40616  cdlemg11aq  40620  cdlemg10a  40622  cdlemg12a  40625  cdlemg12b  40626  cdlemg12c  40627  cdlemg12d  40628  cdlemg13  40634  cdlemg14f  40635  cdlemg14g  40636  cdlemg17b  40644  cdlemg17dN  40645  cdlemg17e  40647  cdlemg17i  40651  cdlemg17pq  40654  cdlemg17iqN  40656  cdlemg18c  40662  cdlemg18d  40663  cdlemg18  40664  cdlemg19  40666  cdlemg21  40668  cdlemg27a  40674  cdlemg31b0N  40676  cdlemg27b  40678  cdlemg31c  40681  cdlemg33b0  40683  cdlemg33c0  40684  cdlemg33  40693  cdlemg35  40695  cdlemg43  40712  cdlemg44a  40713  cdlemg46  40717  cdlemh2  40798  cdlemh  40799  cdlemj1  40803  cdlemk3  40815  cdlemk5  40818  cdlemk6  40819  cdlemki  40823  cdlemksv2  40829  cdlemk12  40832  cdlemk15  40837  cdlemk16  40839  cdlemk18  40850  cdlemk19  40851  cdlemk7u  40852  cdlemk12u  40854  cdlemkoatnle-2N  40857  cdlemk13-2N  40858  cdlemkole-2N  40859  cdlemk14-2N  40860  cdlemk15-2N  40861  cdlemk16-2N  40862  cdlemk17-2N  40863  cdlemk18-2N  40868  cdlemk19-2N  40869  cdlemk7u-2N  40870  cdlemk11u-2N  40871  cdlemk12u-2N  40872  cdlemk20-2N  40874  cdlemk22  40875  cdlemk30  40876  cdlemk31  40878  cdlemk24-3  40885  cdlemkid2  40906  cdlemkfid3N  40907  cdlemk11ta  40911  cdlemkid3N  40915  cdlemk11tc  40927  cdlemk45  40929  cdlemk46  40930  cdlemk47  40931  cdlemk52  40936  cdlemk53a  40937  cdlemk53b  40938  cdleml1N  40958  cdleml3N  40960  cdlemn7  41185  cdlemn10  41188  dihordlem7  41196  dihord1  41200  dihord11c  41206  dihord2  41209  hlhilphllem  41945  fmuldfeq  45538  seposep  48721  iscnrm3rlem8  48743  iscnrm3llem2  48746