Theorem 3imtr4d 554

Description: More general version of 3imtr4i 226. 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 211	. 2 |- (ph -> (ps -> ta))
5	1, 4	sylbid 210	1 |- (ph -> (th -> ta))

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

This theorem is referenced by:  ax11indalem 1410  ax11inda2ALT 1411  unielrel 3571  fconst5 3905  oaord 4239  omord2 4256  omcan 4258  oeord 4273  oecan 4274  omsmo 4315  oprec 4379  pm54.43 4632  ltsopi 5081  axlttrn 5569  axltadd 5570  axmulgt0 5571  axsup 5572  recex 5749  nnge1 6003  uzss 6457  eluzp1m1 6459  expge0 6680  expge1 6682  expcan 6690  expord 6691  expwordi 6692  expword2i 6694  abssubne0 6972  ser1absdiflem 7019  climsqueeze 7230  climsqueeze2 7231  rescncf 7362  cncffvrn 7363  znnen 7594  tgss 7725  neips 7812  cnsscnp 7857  ssbl 7940  opnin 7954  metcnss 7983  metcnss2 7984  caussi 8039  lmcau 8081  sqcn 8419  nmcnilem 8421  spwval 8743  spwnex 8745  ocsh 9239  leopadd 10148  leopmuli 10149  leopmul2i 10151  leoptr 10153  spansncv2 10304  mdsl0 10321  ssdmd1 10324  cvdmd 10348  cdj3i 10452  lediv2aALT 10456  truni1 10593  hmphsyma 10622  homcardus 10634

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 154

Copyright terms: Public domain