Theorem 3imtr4d 543

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 1368  ax11inda2ALT 1369  unielrel 3514  fconst5 3848  oaord 4181  omord2 4198  omcan 4200  oeord 4215  oecan 4216  omsmo 4257  oprec 4318  pm54.43 4572  ltsopi 5016  axlttrn 5504  axltadd 5505  axmulgt0 5506  axsup 5507  recext 5684  nnge1t 5943  uzss 6431  eluzp1m1t 6433  expge0t 6591  expge1t 6593  expcant 6601  expordt 6602  expwordit 6603  expword2it 6605  mulretOLD 6777  abssubne0t 6882  ser1absdiflem 6929  climsqueeze 7140  climsqueeze2 7141  rescncf 7272  cncffvrn 7273  znnen 7502  tgsst 7636  neips 7727  cnsscnp 7772  ssbl 7855  opnin 7869  metcnss 7898  metcnss2 7899  caussi 7954  lmcau 7996  sqcn 8335  nmcnilem 8337  spwval 8659  spwnex 8661  ocsh 9156  leopaddt 10065  leopmulit 10066  leopmul2it 10068  leoptrt 10070  spansncv2t 10220  mdsl0 10237  ssdmd1 10240  cvdmdt 10264  cdj3 10368  lediv2itALT 10371  truni1 10499  hmphsyma 10528  homcardus 10540

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