Theorem simp31 1211

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp131  1310  simp231  1319  simp331  1328  eqfunresadj  7316  smogt  8309  frlmphl  21748  mdetuni0  22577  mdetmul  22579  gsummatr01lem3  22613  decpmatmullem  22727  tsmsxp  24111  log2sumbnd  27523  nosupres  27687  noinfres  27702  ax5seg  29023  wlkoniswlk  29745  iocinioc2  32870  totprob  34605  cgrtr  36208  cgrtr3  36210  ofscom  36223  cgrextend  36224  segconeq  36226  ifscgr  36260  btwnxfr  36272  colinearxfr  36291  brofs2  36293  brifs2  36294  fscgr  36296  btwnconn1lem1  36303  btwnconn1lem2  36304  btwnconn1lem5  36307  btwnconn1lem6  36308  btwnconn1lem7  36309  btwnconn1lem8  36310  btwnconn1lem9  36311  btwnconn1lem10  36312  btwnconn1lem11  36313  btwnconn1lem12  36314  seglecgr12im  36326  seglecgr12  36327  segletr  36330  outsideofeq  36346  ivthALT  36551  lshpkrlem5  39490  lshpkrlem6  39491  exatleN  39780  atbtwn  39822  atbtwnexOLDN  39823  atbtwnex  39824  4noncolr3  39829  3dimlem3a  39836  3dimlem4a  39839  3dim1  39843  3dim2  39844  1cvrat  39852  2atjlej  39855  hlatexch4  39857  ps-2b  39858  2atm  39903  2atmat  39937  4atlem11b  39984  4atlem11  39985  4at  39989  4at2  39990  2lplnja  39995  2lplnj  39996  dalemswapyz  40032  dalemccnedd  40063  cdlemb  40170  paddasslem5  40200  paddasslem15  40210  pmodlem1  40222  dalawlem1  40247  dalawlem3  40249  dalawlem4  40250  dalawlem5  40251  dalawlem6  40252  dalawlem7  40253  dalawlem8  40254  dalawlem9  40255  dalawlem11  40257  dalawlem12  40258  dalawlem15  40261  osumcllem5N  40336  osumcllem6N  40337  lhpexle3lem  40387  lhpmcvr4N  40402  lhpmcvr6N  40404  4atex2  40453  4atex2-0bOLDN  40455  4atex3  40457  ltrn11at  40523  trlval3  40563  cdlemd3  40576  cdleme0moN  40601  cdleme7aa  40618  cdleme7b  40620  cdleme7c  40621  cdleme7d  40622  cdleme7e  40623  cdleme7ga  40624  cdleme7  40625  cdleme16aN  40635  cdleme11dN  40638  cdleme11e  40639  cdleme11l  40645  cdleme11  40646  cdleme12  40647  cdleme14  40649  cdleme15b  40651  cdleme15c  40652  cdleme16b  40655  cdleme16c  40656  cdleme16d  40657  cdleme16e  40658  cdleme16f  40659  cdleme17c  40664  cdleme18c  40669  cdleme18d  40671  cdlemeda  40674  cdleme19a  40679  cdleme19b  40680  cdleme19c  40681  cdleme20aN  40685  cdleme20bN  40686  cdleme20d  40688  cdleme20i  40693  cdleme20j  40694  cdleme20l1  40696  cdleme20l2  40697  cdleme21d  40706  cdleme21e  40707  cdleme21f  40708  cdleme22aa  40715  cdleme22e  40720  cdleme22eALTN  40721  cdleme22f2  40723  cdleme22g  40724  cdleme23b  40726  cdleme26eALTN  40737  cdleme26fALTN  40738  cdleme26f  40739  cdleme26f2ALTN  40740  cdleme26f2  40741  cdleme28a  40746  cdleme28b  40747  cdleme32b  40818  cdleme32c  40819  cdleme32e  40821  cdleme35h  40832  cdleme35sn2aw  40834  cdleme41sn3aw  40850  cdleme41sn4aw  40851  cdlemeg46gfre  40908  cdlemf1  40937  cdlemg1cex  40964  cdlemg2ce  40968  cdlemg4d  40989  cdlemg4e  40990  cdlemg4f  40991  cdlemg4  40993  cdlemg6d  40997  cdlemg6e  40998  cdlemg7fvN  41000  cdlemg8b  41004  cdlemg8c  41005  cdlemg9a  41008  cdlemg9b  41009  cdlemg9  41010  cdlemg11aq  41014  cdlemg10a  41016  cdlemg12a  41019  cdlemg12b  41020  cdlemg12c  41021  cdlemg12d  41022  cdlemg13  41028  cdlemg14f  41029  cdlemg14g  41030  cdlemg17b  41038  cdlemg17dN  41039  cdlemg17e  41041  cdlemg17i  41045  cdlemg17pq  41048  cdlemg17iqN  41050  cdlemg18c  41056  cdlemg18d  41057  cdlemg18  41058  cdlemg19  41060  cdlemg21  41062  cdlemg27a  41068  cdlemg31b0N  41070  cdlemg27b  41072  cdlemg31c  41075  cdlemg33b0  41077  cdlemg33c0  41078  cdlemg33  41087  cdlemg35  41089  cdlemg43  41106  cdlemg44a  41107  cdlemg46  41111  cdlemh2  41192  cdlemh  41193  cdlemj1  41197  cdlemk3  41209  cdlemk5  41212  cdlemk6  41213  cdlemki  41217  cdlemksv2  41223  cdlemk12  41226  cdlemk15  41231  cdlemk16  41233  cdlemk18  41244  cdlemk19  41245  cdlemk7u  41246  cdlemk12u  41248  cdlemkoatnle-2N  41251  cdlemk13-2N  41252  cdlemkole-2N  41253  cdlemk14-2N  41254  cdlemk15-2N  41255  cdlemk16-2N  41256  cdlemk17-2N  41257  cdlemk18-2N  41262  cdlemk19-2N  41263  cdlemk7u-2N  41264  cdlemk11u-2N  41265  cdlemk12u-2N  41266  cdlemk20-2N  41268  cdlemk22  41269  cdlemk30  41270  cdlemk31  41272  cdlemk24-3  41279  cdlemkid2  41300  cdlemkfid3N  41301  cdlemk11ta  41305  cdlemkid3N  41309  cdlemk11tc  41321  cdlemk45  41323  cdlemk46  41324  cdlemk47  41325  cdlemk52  41330  cdlemk53a  41331  cdlemk53b  41332  cdleml1N  41352  cdleml3N  41354  cdlemn7  41579  cdlemn10  41582  dihordlem7  41590  dihord1  41594  dihord11c  41600  dihord2  41603  hlhilphllem  42335  fmuldfeq  45943  seposep  49285  iscnrm3rlem8  49306  iscnrm3llem2  49309