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

Syntax hints:   → wi 4   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  simp131  1309  simp231  1318  simp331  1327  eqfunresadj  7357  smogt  8367  frlmphl  21336  mdetuni0  22123  mdetmul  22125  gsummatr01lem3  22159  decpmatmullem  22273  tsmsxp  23659  log2sumbnd  27047  nosupres  27210  noinfres  27225  ax5seg  28227  wlkoniswlk  28949  iocinioc2  32021  totprob  33457  cgrtr  34995  cgrtr3  34997  ofscom  35010  cgrextend  35011  segconeq  35013  ifscgr  35047  btwnxfr  35059  colinearxfr  35078  brofs2  35080  brifs2  35081  fscgr  35083  btwnconn1lem1  35090  btwnconn1lem2  35091  btwnconn1lem5  35094  btwnconn1lem6  35095  btwnconn1lem7  35096  btwnconn1lem8  35097  btwnconn1lem9  35098  btwnconn1lem10  35099  btwnconn1lem11  35100  btwnconn1lem12  35101  seglecgr12im  35113  seglecgr12  35114  segletr  35117  outsideofeq  35133  ivthALT  35268  lshpkrlem5  38032  lshpkrlem6  38033  exatleN  38323  atbtwn  38365  atbtwnexOLDN  38366  atbtwnex  38367  4noncolr3  38372  3dimlem3a  38379  3dimlem4a  38382  3dim1  38386  3dim2  38387  1cvrat  38395  2atjlej  38398  hlatexch4  38400  ps-2b  38401  2atm  38446  2atmat  38480  4atlem11b  38527  4atlem11  38528  4at  38532  4at2  38533  2lplnja  38538  2lplnj  38539  dalemswapyz  38575  dalemccnedd  38606  cdlemb  38713  paddasslem5  38743  paddasslem15  38753  pmodlem1  38765  dalawlem1  38790  dalawlem3  38792  dalawlem4  38793  dalawlem5  38794  dalawlem6  38795  dalawlem7  38796  dalawlem8  38797  dalawlem9  38798  dalawlem11  38800  dalawlem12  38801  dalawlem15  38804  osumcllem5N  38879  osumcllem6N  38880  lhpexle3lem  38930  lhpmcvr4N  38945  lhpmcvr6N  38947  4atex2  38996  4atex2-0bOLDN  38998  4atex3  39000  ltrn11at  39066  trlval3  39106  cdlemd3  39119  cdleme0moN  39144  cdleme7aa  39161  cdleme7b  39163  cdleme7c  39164  cdleme7d  39165  cdleme7e  39166  cdleme7ga  39167  cdleme7  39168  cdleme16aN  39178  cdleme11dN  39181  cdleme11e  39182  cdleme11l  39188  cdleme11  39189  cdleme12  39190  cdleme14  39192  cdleme15b  39194  cdleme15c  39195  cdleme16b  39198  cdleme16c  39199  cdleme16d  39200  cdleme16e  39201  cdleme16f  39202  cdleme17c  39207  cdleme18c  39212  cdleme18d  39214  cdlemeda  39217  cdleme19a  39222  cdleme19b  39223  cdleme19c  39224  cdleme20aN  39228  cdleme20bN  39229  cdleme20d  39231  cdleme20i  39236  cdleme20j  39237  cdleme20l1  39239  cdleme20l2  39240  cdleme21d  39249  cdleme21e  39250  cdleme21f  39251  cdleme22aa  39258  cdleme22e  39263  cdleme22eALTN  39264  cdleme22f2  39266  cdleme22g  39267  cdleme23b  39269  cdleme26eALTN  39280  cdleme26fALTN  39281  cdleme26f  39282  cdleme26f2ALTN  39283  cdleme26f2  39284  cdleme28a  39289  cdleme28b  39290  cdleme32b  39361  cdleme32c  39362  cdleme32e  39364  cdleme35h  39375  cdleme35sn2aw  39377  cdleme41sn3aw  39393  cdleme41sn4aw  39394  cdlemeg46gfre  39451  cdlemf1  39480  cdlemg1cex  39507  cdlemg2ce  39511  cdlemg4d  39532  cdlemg4e  39533  cdlemg4f  39534  cdlemg4  39536  cdlemg6d  39540  cdlemg6e  39541  cdlemg7fvN  39543  cdlemg8b  39547  cdlemg8c  39548  cdlemg9a  39551  cdlemg9b  39552  cdlemg9  39553  cdlemg11aq  39557  cdlemg10a  39559  cdlemg12a  39562  cdlemg12b  39563  cdlemg12c  39564  cdlemg12d  39565  cdlemg13  39571  cdlemg14f  39572  cdlemg14g  39573  cdlemg17b  39581  cdlemg17dN  39582  cdlemg17e  39584  cdlemg17i  39588  cdlemg17pq  39591  cdlemg17iqN  39593  cdlemg18c  39599  cdlemg18d  39600  cdlemg18  39601  cdlemg19  39603  cdlemg21  39605  cdlemg27a  39611  cdlemg31b0N  39613  cdlemg27b  39615  cdlemg31c  39618  cdlemg33b0  39620  cdlemg33c0  39621  cdlemg33  39630  cdlemg35  39632  cdlemg43  39649  cdlemg44a  39650  cdlemg46  39654  cdlemh2  39735  cdlemh  39736  cdlemj1  39740  cdlemk3  39752  cdlemk5  39755  cdlemk6  39756  cdlemki  39760  cdlemksv2  39766  cdlemk12  39769  cdlemk15  39774  cdlemk16  39776  cdlemk18  39787  cdlemk19  39788  cdlemk7u  39789  cdlemk12u  39791  cdlemkoatnle-2N  39794  cdlemk13-2N  39795  cdlemkole-2N  39796  cdlemk14-2N  39797  cdlemk15-2N  39798  cdlemk16-2N  39799  cdlemk17-2N  39800  cdlemk18-2N  39805  cdlemk19-2N  39806  cdlemk7u-2N  39807  cdlemk11u-2N  39808  cdlemk12u-2N  39809  cdlemk20-2N  39811  cdlemk22  39812  cdlemk30  39813  cdlemk31  39815  cdlemk24-3  39822  cdlemkid2  39843  cdlemkfid3N  39844  cdlemk11ta  39848  cdlemkid3N  39852  cdlemk11tc  39864  cdlemk45  39866  cdlemk46  39867  cdlemk47  39868  cdlemk52  39873  cdlemk53a  39874  cdlemk53b  39875  cdleml1N  39895  cdleml3N  39897  cdlemn7  40122  cdlemn10  40125  dihordlem7  40133  dihord1  40137  dihord11c  40143  dihord2  40146  hlhilphllem  40882  fmuldfeq  44347  seposep  47606  iscnrm3rlem8  47628  iscnrm3llem2  47631