Theorem 3imtr4 219

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 199	. 2 |- (ch -> ps)
4		3imtr4.3	. 2 |- (th <-> ps)
5	3, 4	sylibr 200	1 |- (ch -> th)

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

This theorem is referenced by:  orim12i 336  pm5.18 662  orbidi 745  3anim123i 823  hbex 1008  hbor 1010  hban 1011  hbbi 1012  hb3or 1013  hb3an 1014  hbe1 1018  19.29 1073  19.29r 1074  19.30 1087  sbimi 1175  sbequ12r 1184  hbeu1 1390  hbeu 1391  hbmo1 1408  hbmo 1409  mopick2 1439  2exeu 1449  2eu6 1457  hbab1 1469  hbab 1470  hbxfr 1566  hbeq 1568  hbel 1569  hbne 1647  hbral 1689  hbra1 1690  hbrex 1691  hbre1 1692  r19.20i2 1706  r19.22 1734  r19.22i2 1736  r19.27av 1757  r19.28av 1758  r19.29 1759  r19.29r 1760  hbreu1 1771  ralcom2 1779  reurex 1931  hbsbc1v 1953  sbcco2 1956  hbss 2065  sseq1 2085  sseq2 2086  rabss2 2132  hbdif 2164  hbun 2189  unss1 2202  hbin 2223  ssin 2235  ssrin 2237  undif4 2329  ralf0 2363  hbpw 2411  hbpr 2430  difprsn 2469  snsspw 2483  hbuni 2513  uniin 2524  hbint 2547  intss 2558  iuniin 2577  iuneq1 2579  iuneq2 2582  iinss 2604  iunpwss 2623  hbbr 2663  unipw 2762  exss 2775  opprc3 2803  hbopab 2818  pwunss 2832  poeq2 2849  soeq2 2860  reucl 2891  freq2 2929  trssord 2971  onminex 3026  hbsuc 3046  nlimsucg 3118  find 3161  hbxp 3210  xpss 3236  hbrel 3251  cnveq 3298  hbcnv 3301  dmeq 3317  dmin 3324  hbrn 3357  dmcosseq 3371  rncoeq 3373  resiexg 3402  hbima 3417  cotr 3442  dminss 3468  imainss 3469  funeq 3541  hbfun 3542  fununi 3569  funin 3572  hbfn 3590  2elresin 3604  zfrep6 3620  hbf 3631  hbf1 3669  f1co 3673  hbfo 3677  fof 3678  foco 3688  hbf1o 3693  f1ocnv 3707  f1ores 3709  f1oco 3713  fopab2 3829  hbiso 3898  isocnv 3902  isotr 3903  isotrALT 3904  tz7.48lem 3961  ider 4275  eqer 4277  map0 4350  ixpeq2 4361  enssdom 4389  sbthlem9 4461  mapunen 4508  zfreg 4605  zfreg2 4606  dfom3 4639  infensuc 4648  scott0 4727  ac6n 4767  ac9s 4774  dominf 4915  dominfOLD 4916  cdainf 4949  ltsopq 5087  1pr 5129  reclem2pr 5169  ltsosr 5215  ltsor 5273  ltadd2 5602  recgt0i 5816  ltmul1i 5823  peano2nn 5937  sup2 6053  peano2uz2 6203  zqt 6261  elioc2t 6391  elico2t 6392  elicc2t 6393  eluzp1p1t 6436  peano2uz 6448  sumsqne0 6635  nnesq 6663  recvalz 6887  cjdiv 6888  cau5i 6917  fsumser0f 7001  fsumser1f 7002  ser0cj 7065  climcmplem 7137  efltb 7407  reeff1o 7426  sin02gt0 7479  infxpidmlem10 7562  indistop 7645  fctopOLD 7647  cctop 7649  retopbas 7652  blssioo 7910  ablmul 8127  sspval 8378  cosh111lem2 8710  efifolem4 8720  efifo 8724  efif1lem1 8725  efif1lem2 8726  axhcompl 8863  hhcmpl 9064  chsscm 9107  chcmh 9108  shscl 9276  shunss 9332  shslej 9333  shlub 9341  pjoml3 9524  cmcmlem 9529  nonbool 9591  5oalem2 9595  3oalem2 9603  lnopco0 9924  bra11 10036  pjnmop 10070  pjnormss 10091  pj3lem1 10129  mdsldmd1 10253  hatomistic 10284  cvexch 10291  cmdmd 10339  mddmdin0 10353  cdj3lem3b 10362  symgf 10400  symggrpi 10401  fine 10442  abfi 10443  neiopne 10463  eqindhome 10527

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