Theorem simp33 1218

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp33	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏)

Proof of Theorem simp33

Step	Hyp	Ref	Expression
1		simp3 1144	. 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:  simp133  1317  simp233  1326  simp333  1335  eqfunresadj  7304  smogt  8297  bitsfzo  16395  frlmphl  21756  mdetunilem4  22598  mdetuni0  22604  mdetmul  22606  decpmatmullem  22754  logexprlim  27206  noinfres  27704  ax5seg  29025  iocinioc2  32871  bnj966  35126  cgrtr  36220  cgrtr3  36222  ofscom  36235  segconeq  36238  btwnxfr  36284  colinearxfr  36303  fscgr  36308  btwnconn1lem1  36315  btwnconn1lem2  36316  btwnconn1lem5  36319  btwnconn1lem6  36320  btwnconn1lem8  36322  btwnconn1lem9  36323  btwnconn1lem10  36324  btwnconn1lem11  36325  btwnconn1lem12  36326  brsegle2  36337  seglecgr12im  36338  seglecgr12  36339  segletr  36342  outsideofeq  36358  lshpkrlem5  39606  lshpkrlem6  39607  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  ps-2c  40020  lvolex3N  40030  2atmat  40053  lvolnlelpln  40077  4atlem10  40098  4atlem11b  40100  4atlem11  40101  4at  40105  4at2  40106  2lplnja  40111  2lplnj  40112  dalemclccjdd  40180  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  4atexlemex6  40566  4atex2  40569  4atex2-0bOLDN  40571  4atex3  40573  ltrn11at  40639  cdlemd3  40692  cdleme7aa  40734  cdleme7b  40736  cdleme7c  40737  cdleme7d  40738  cdleme7ga  40740  cdleme16aN  40751  cdleme11dN  40754  cdleme11e  40755  cdleme11l  40761  cdleme11  40762  cdleme12  40763  cdleme14  40765  cdleme15c  40768  cdleme16b  40771  cdleme16d  40773  cdleme17b  40779  cdleme17c  40780  cdleme18c  40785  cdleme18d  40787  cdlemeda  40790  cdlemednpq  40791  cdleme19a  40795  cdleme19c  40797  cdleme20aN  40801  cdleme20bN  40802  cdleme20d  40804  cdleme20f  40806  cdleme20g  40807  cdleme20j  40810  cdleme20l1  40812  cdleme21f  40824  cdleme22aa  40831  cdleme22a  40832  cdleme22cN  40834  cdleme22e  40836  cdleme22f2  40839  cdleme22g  40840  cdleme23b  40842  cdleme23c  40843  cdleme26e  40851  cdleme26fALTN  40854  cdleme26f  40855  cdleme26f2ALTN  40856  cdleme26f2  40857  cdleme28a  40862  cdleme28b  40863  cdleme32b  40934  cdleme32c  40935  cdleme32e  40937  cdleme35h2  40949  cdleme38m  40955  cdleme41sn4aw  40967  cdlemf1  41053  cdlemg1cex  41080  cdlemg2ce  41084  cdlemg4d  41105  cdlemg4f  41107  cdlemg7fvN  41116  cdlemg8a  41119  cdlemg8b  41120  cdlemg8c  41121  cdlemg9a  41124  cdlemg11a  41129  cdlemg11aq  41130  cdlemg10a  41132  cdlemg11b  41134  cdlemg12a  41135  cdlemg12b  41136  cdlemg12d  41138  cdlemg12e  41139  cdlemg12f  41140  cdlemg12g  41141  cdlemg12  41142  cdlemg13a  41143  cdlemg13  41144  cdlemg14f  41145  cdlemg14g  41146  cdlemg17b  41154  cdlemg17dN  41155  cdlemg17e  41157  cdlemg17h  41160  cdlemg17pq  41164  cdlemg17iqN  41166  cdlemg18b  41171  cdlemg18c  41172  cdlemg18d  41173  cdlemg18  41174  cdlemg19  41176  cdlemg21  41178  cdlemg27a  41184  cdlemg31b0N  41186  cdlemg27b  41188  cdlemg33b0  41193  cdlemg33c0  41194  cdlemg28  41196  cdlemg33a  41198  cdlemg35  41205  cdlemg42  41221  cdlemg44a  41223  cdlemg47  41228  cdlemh2  41308  cdlemh  41309  cdlemj1  41313  cdlemk3  41325  cdlemk5  41328  cdlemki  41333  cdlemksv2  41339  cdlemk7  41340  cdlemk11  41341  cdlemk12  41342  cdlemkole  41345  cdlemk14  41346  cdlemk15  41347  cdlemk16a  41348  cdlemk16  41349  cdlemkj  41355  cdlemkuv2  41359  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  cdlemk21-2N  41383  cdlemk20-2N  41384  cdlemk22  41385  cdlemk30  41386  cdlemk31  41388  cdlemk32  41389  cdlemk24-3  41395  cdlemkid2  41416  cdlemkfid3N  41417  cdlemk45  41439  cdlemk46  41440  cdlemk47  41441  cdlemk52  41446  cdlemk53a  41447  cdleml1N  41468  cdleml3N  41470  cdlemn7  41695  cdlemn10  41698  dihordlem7  41706  dihord1  41710  dihord2a  41711  dihord10  41715  dihord11c  41716  dihord2pre2  41718  hlhilphllem  42451  fmuldfeq  46028  usgrgrtrirex  48441  grlimprclnbgredg  48488  seposep  49416  iscnrm3rlem8  49437  iscnrm3llem2  49440