Theorem 3imtr4 192

Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication.

Hypotheses

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

Assertion

Ref	Expression
3imtr4	|- (ch -> th)

Proof of Theorem 3imtr4

Step	Hyp	Ref	Expression
1		3imtr4.2	. . 3 |- (ch <-> ph)
2		3imtr4.1	. . 3 |- (ph -> ps)
3	1, 2	sylbi 174	. 2 |- (ch -> ps)
4		3imtr4.3	. 2 |- (th <-> ps)
5	3, 4	sylibr 175	1 |- (ch -> th)

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  orim12i 271  pm5.18 497  orbidi 510  im3an 605  hbex 701  hbor 703  hban 704  hbbi 705  hb3or 706  hb3an 707  hbe1 709  19.29 752  19.29r 753  19.30 764  sbimi 854  sbequ12r 866  hbeu1 1015  hbeu 1016  hbmo1 1032  hbmo 1033  mopick2 1057  2exeu 1066  hbab1 1095  hbab 1096  hbeq 1171  hbel 1172  hbral 1236  hbra1 1237  hbrex 1238  hbre1 1239  r19.20i2 1252  r19.22 1272  r19.22i2 1274  r19.27av 1293  r19.28av 1294  r19.29 1295  r19.29r 1296  hbreu1 1307  hbrab1 1310  hbrab 1311  ralcom2 1314  reurex 1337  hbsbcv 1447  sbcco2 1449  hbss 1501  sseq1 1521  sseq2 1522  hbdif 1590  hbun 1614  unss1 1627  hbin 1647  ssin 1659  ssrin 1661  undif4 1744  hbpw 1804  hbpr 1824  hbsn 1833  snsspw 1857  hbop 1879  exss 1881  opprc3 1908  pwunss 1916  hbuni 1925  uniin 1935  reucl 1957  unipw 1960  hbint 1975  intss 1983  iuniin 2001  iuneq1 2003  iuneq2 2006  hbiu1 2012  hbii1 2013  iinss 2025  iunpwss 2039  hbbr 2095  hbopab 2111  hbopab1 2112  hbopab2 2113  poeq2 2131  soeq2 2142  freq2 2175  trssord 2216  tfi 2244  onminex 2275  hbsuc 2294  nlimsuc 2363  find 2396  hbxp 2444  xpss 2465  hbrel 2478  hbco 2508  cnveq 2513  hbcnv 2516  dmeq 2531  dmin 2537  hbrn 2564  hbdm 2565  dmcosseq 2572  rncoeq 2574  hbres 2577  hbima 2609  cotr 2625  dminss 2648  imainss 2649  funeq 2683  hbfun 2684  fununi 2705  funin 2708  hbfn 2720  2elresin 2733  zfrep6 2744  fnopabg 2745  hbf 2751  hbf1 2779  f1co 2783  hbfo 2787  fof 2788  hbf1o 2798  f1ocnv 2811  f1ores 2813  f1oco 2816  hbfv 2837  elrnopab 2884  fopab2 2891  hbiso 2930  isocnv 2934  isotr 2935  isotrALT 2936  hbrdg 2974  tz7.48lem 2993  abianfplem 2999  hbopr 3017  hboprab1 3023  hboprab2 3024  elrnoprab 3054  ider 3208  map0 3268  enssdom 3287  sbthlem9 3357  xpmapenlem1 3391  xpmapenlem4 3394  mapunen 3397  zfreg 3447  zfreg2 3448  dfom3 3477  infensuc 3484  trcl 3489  tz9.12lem3 3505  scott0 3542  ac6lem 3575  hta 3619  cdainf 3731  ltsopq 3869  1pr 3911  reclem2pr 3951  ltsosr 3997  ltsor 4055  axrecex 4079  recgt0i 4385  peano2nn 4433  sup2 4510  peano2uz 4602  zqt 4632  om2uzsuc 4652  sqegt0 4703  nnesq 4720  infxpidmlem10 4942  chsscm 5147  chcmh 5148  shscl 5282  shunss 5338  shslej 5339  shlub 5347  pjoml3 5496  cmcmlem 5500  5oalem2 5545  3oalem2 5553  pjnormss 5638  pj3lem1 5658  hatomistic 5755  cvexch 5760

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

This theorem depends on definitions:  df-bi 128

metamath.org