Theorem simp31 1090

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simpl31  1135  simpr31  1144  simp131  1189  simp231  1198  simp331  1207  smogt  7351  frlmphl  19939  mdetuni0  20246  mdetmul  20248  gsummatr01lem3  20282  decpmatmullem  20395  tsmsxp  21768  log2sumbnd  25033  ax5seg  25618  iocinioc2  28931  totprob  29816  cgrtr  31269  cgrtr3  31271  ofscom  31284  cgrextend  31285  segconeq  31287  ifscgr  31321  btwnxfr  31333  colinearxfr  31352  brofs2  31354  brifs2  31355  fscgr  31357  btwnconn1lem1  31364  btwnconn1lem2  31365  btwnconn1lem5  31368  btwnconn1lem6  31369  btwnconn1lem7  31370  btwnconn1lem8  31371  btwnconn1lem9  31372  btwnconn1lem10  31373  btwnconn1lem11  31374  btwnconn1lem12  31375  seglecgr12im  31387  seglecgr12  31388  segletr  31391  outsideofeq  31407  ivthALT  31500  lshpkrlem5  33419  lshpkrlem6  33420  exatleN  33708  atbtwn  33750  atbtwnexOLDN  33751  atbtwnex  33752  4noncolr3  33757  3dimlem3a  33764  3dimlem4a  33767  3dim1  33771  3dim2  33772  1cvrat  33780  2atjlej  33783  hlatexch4  33785  ps-2b  33786  2atm  33831  2atmat  33865  4atlem11b  33912  4atlem11  33913  4at  33917  4at2  33918  2lplnja  33923  2lplnj  33924  dalemswapyz  33960  dalemccnedd  33991  cdlemb  34098  paddasslem5  34128  paddasslem15  34138  pmodlem1  34150  dalawlem1  34175  dalawlem3  34177  dalawlem4  34178  dalawlem5  34179  dalawlem6  34180  dalawlem7  34181  dalawlem8  34182  dalawlem9  34183  dalawlem11  34185  dalawlem12  34186  dalawlem15  34189  osumcllem5N  34264  osumcllem6N  34265  lhpexle3lem  34315  lhpmcvr4N  34330  lhpmcvr6N  34332  4atex2  34381  4atex2-0bOLDN  34383  4atex3  34385  ltrn11at  34451  trlval3  34492  cdlemd3  34505  cdleme0moN  34530  cdleme7aa  34547  cdleme7b  34549  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme16aN  34564  cdleme11dN  34567  cdleme11e  34568  cdleme11l  34574  cdleme11  34575  cdleme12  34576  cdleme14  34578  cdleme15b  34580  cdleme15c  34581  cdleme16b  34584  cdleme16c  34585  cdleme16d  34586  cdleme16e  34587  cdleme16f  34588  cdleme17c  34593  cdleme18c  34598  cdleme18d  34600  cdlemeda  34603  cdleme19a  34609  cdleme19b  34610  cdleme19c  34611  cdleme20aN  34615  cdleme20bN  34616  cdleme20d  34618  cdleme20i  34623  cdleme20j  34624  cdleme20l1  34626  cdleme20l2  34627  cdleme21d  34636  cdleme21e  34637  cdleme21f  34638  cdleme22aa  34645  cdleme22e  34650  cdleme22eALTN  34651  cdleme22f2  34653  cdleme22g  34654  cdleme23b  34656  cdleme26eALTN  34667  cdleme26fALTN  34668  cdleme26f  34669  cdleme26f2ALTN  34670  cdleme26f2  34671  cdleme28a  34676  cdleme28b  34677  cdleme32b  34748  cdleme32c  34749  cdleme32e  34751  cdleme35h  34762  cdleme35sn2aw  34764  cdleme41sn3aw  34780  cdleme41sn4aw  34781  cdlemeg46gfre  34838  cdlemf1  34867  cdlemg1cex  34894  cdlemg2ce  34898  cdlemg4d  34919  cdlemg4e  34920  cdlemg4f  34921  cdlemg4  34923  cdlemg6d  34927  cdlemg6e  34928  cdlemg7fvN  34930  cdlemg8b  34934  cdlemg8c  34935  cdlemg9a  34938  cdlemg9b  34939  cdlemg9  34940  cdlemg11aq  34944  cdlemg10a  34946  cdlemg12a  34949  cdlemg12b  34950  cdlemg12c  34951  cdlemg12d  34952  cdlemg13  34958  cdlemg14f  34959  cdlemg14g  34960  cdlemg17b  34968  cdlemg17dN  34969  cdlemg17e  34971  cdlemg17i  34975  cdlemg17pq  34978  cdlemg17iqN  34980  cdlemg18c  34986  cdlemg18d  34987  cdlemg18  34988  cdlemg19  34990  cdlemg21  34992  cdlemg27a  34998  cdlemg31b0N  35000  cdlemg27b  35002  cdlemg31c  35005  cdlemg33b0  35007  cdlemg33c0  35008  cdlemg33  35017  cdlemg35  35019  cdlemg43  35036  cdlemg44a  35037  cdlemg46  35041  cdlemh2  35122  cdlemh  35123  cdlemj1  35127  cdlemk3  35139  cdlemk5  35142  cdlemk6  35143  cdlemki  35147  cdlemksv2  35153  cdlemk12  35156  cdlemk15  35161  cdlemk16  35163  cdlemk18  35174  cdlemk19  35175  cdlemk7u  35176  cdlemk12u  35178  cdlemkoatnle-2N  35181  cdlemk13-2N  35182  cdlemkole-2N  35183  cdlemk14-2N  35184  cdlemk15-2N  35185  cdlemk16-2N  35186  cdlemk17-2N  35187  cdlemk18-2N  35192  cdlemk19-2N  35193  cdlemk7u-2N  35194  cdlemk11u-2N  35195  cdlemk12u-2N  35196  cdlemk20-2N  35198  cdlemk22  35199  cdlemk30  35200  cdlemk31  35202  cdlemk24-3  35209  cdlemkid2  35230  cdlemkfid3N  35231  cdlemk11ta  35235  cdlemkid3N  35239  cdlemk11tc  35251  cdlemk45  35253  cdlemk46  35254  cdlemk47  35255  cdlemk52  35260  cdlemk53a  35261  cdlemk53b  35262  cdleml1N  35282  cdleml3N  35284  cdlemn7  35510  cdlemn10  35513  dihordlem7  35521  dihord1  35525  dihord11c  35531  dihord2  35534  hlhilphllem  36269  fmuldfeq  38650  wlkOniswlk  40869