Theorem 3imtr4d 541

Description: More general version of 3imtr4 219. 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 204	. 2 |- (ph -> (ps -> ta))
5	1, 4	sylbid 203	1 |- (ph -> (th -> ta))

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

This theorem is referenced by:  ax11indalem 1361  ax11inda2ALT 1362  unielrel 3500  fconst5 3833  oaord 4165  omord2 4182  omcan 4184  oeord 4199  oecan 4200  omsmo 4241  oprec 4302  pm54.43 4546  ltsopi 4988  axlttrn 5476  axltadd 5477  axmulgt0 5478  axsup 5479  recext 5657  nnge1t 5891  uzss 6363  eluzp1m1t 6365  expge0t 6522  expge1t 6524  expcant 6532  expordt 6533  expwordit 6534  expword2it 6536  abssubne0t 6820  ser1absdiflem 6866  climsqueeze 7076  climsqueeze2 7077  rescncf 7207  cncffvrn 7208  znnen 7445  tgsst 7578  neips 7668  cnsscnp 7711  ssbl 7795  opnin 7809  metcnss 7837  metcnss2 7838  caussi 7889  lmcau 7930  sqcn 8270  nmcnilem 8272  spwval 8582  ocsh 9072  leopaddt 9977  leopmulit 9978  leopmul2it 9980  spansncv2t 10130  mdsl0 10145  ssdmd1 10148  cvdmdt 10172  cdj3 10273  lediv2itALT 10276  truni1 10386  hmphsyma 10415

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 147

Copyright terms: Public domain