Theorem 3imtr4d 546

Description: More general version of 3imtr4i 217. Useful for converting conditional definitions in a formula.

Hypotheses

Ref	Expression
3imtr4d.1	|- (ph -> (ps -> ch))
3imtr4d.2	|- (ph -> (th <-> ps))
3imtr4d.3	|- (ph -> (ta <-> ch))

Assertion

Ref	Expression
3imtr4d	|- (ph -> (th -> ta))

Proof of Theorem 3imtr4d

Step	Hyp	Ref	Expression
1		3imtr4d.2	. 2 |- (ph -> (th <-> ps))
2		3imtr4d.1	. . 3 |- (ph -> (ps -> ch))
3		3imtr4d.3	. . 3 |- (ph -> (ta <-> ch))
4	2, 3	sylibrd 202	. 2 |- (ph -> (ps -> ta))
5	1, 4	sylbid 201	1 |- (ph -> (th -> ta))

Syntax hints:   -> wi 3   <-> wb 144

This theorem is referenced by:  ax11indalem 1407  ax11inda2ALT 1408  unielrel 3619  fconst5 3962  oaord 4317  omord2 4334  omcan 4336  oeord 4351  oecan 4352  omsmo 4397  oprec 4459  pm54.43 4715  ltsopi 5170  axlttrn 5658  axltadd 5659  axmulgt0 5660  axsup 5661  recex 5840  nnge1 6088  uzss 6558  eluzp1m1 6560  expge0 6785  expge1 6787  expcan 6798  expord 6799  expwordi 6800  expword2i 6802  abssubne0 7085  ser1absdiflem 7132  climsqueeze 7343  climsqueeze2 7344  rescncf 7477  cncffvrn 7478  znnen 7714  tgss 7848  neips 7937  cnsscnp 7982  ssbl 8065  opnin 8079  metcnss 8109  metcnss2 8110  caussi 8165  lmcau 8207  sqcn 8589  nmcnilem 8591  spwval 8921  spwnex 8923  ocsh 9432  leopadd 10345  leopmuli 10346  leopmul2i 10348  leoptr 10350  spansncv2 10501  mdsl0 10518  ssdmd1 10521  cvdmd 10545  cdj3i 10650  lediv2aALT 10656  njtlc 10804  truni1 10999  hmphsyma 11034  homcardus 11046  elomsubsd 11446  omsublim 11448  opnnei 11469  subtopmetlem 11505  iccconn 11514  ivthALT 11515  lfinpfin 11574  fnejoin2 11592  fgss 11634  fgfil 11638  fbfgss 11640  limfilss 11682  flimfcls 11725  fcluscnplem 11729  fcluscnp 11730  dirge 11754  tailfb 11762  incsequz 11879  lpss2 11906  iccss 11920  cnss 11953  hmeocn 11958  hmeocnv 11959  txsubsp 11983  txcld 11985  totbndss 11993  totbndbnd 12000  ismtycnv 12005  ismtyhmeolem 12006  ismtyhmeo 12007  ismtybndlem 12008  ismtyres 12010  heiborlem42 12052  rrncms 12075  rrntotbnd 12078  phtpycom 12092  phtpyco 12098  phtpcer 12104

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145

Copyright terms: Public domain