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 658  orbidi 741  3anim123i 819  hbex 1003  hbor 1005  hban 1006  hbbi 1007  hb3or 1008  hb3an 1009  hbe1 1012  19.29 1067  19.29r 1068  19.30 1081  sbimi 1169  sbequ12r 1178  hbeu1 1381  hbeu 1382  hbmo1 1399  hbmo 1400  mopick2 1429  2exeu 1439  2eu6 1447  hbab1 1459  hbab 1460  hbxfr 1555  hbeq 1557  hbel 1558  hbne 1636  hbral 1678  hbra1 1679  hbrex 1680  hbre1 1681  r19.20i2 1695  r19.22 1723  r19.22i2 1725  r19.27av 1746  r19.28av 1747  r19.29 1748  r19.29r 1749  hbreu1 1760  ralcom2 1768  reurex 1918  hbsbc1v 1940  sbcco2 1943  hbss 2052  sseq1 2072  sseq2 2073  rabss2 2119  hbdif 2151  hbun 2176  unss1 2189  hbin 2210  ssin 2222  ssrin 2224  undif4 2315  ralf0 2349  hbpw 2397  hbpr 2416  difprsn 2456  snsspw 2470  hbuni 2499  uniin 2510  hbint 2533  intss 2544  iuniin 2563  iuneq1 2565  iuneq2 2568  iinss 2590  iunpwss 2608  hbbr 2648  unipw 2746  exss 2759  opprc3 2787  hbopab 2801  pwunss 2815  poeq2 2834  soeq2 2845  reucl 2875  freq2 2913  trssord 2955  onminex 3010  hbsuc 3030  nlimsucg 3102  find 3145  hbxp 3194  xpss 3220  hbrel 3235  cnveq 3281  hbcnv 3284  dmeq 3300  dmin 3307  hbrn 3337  dmcosseq 3349  rncoeq 3351  resiexg 3380  hbima 3395  cotr 3420  dminss 3448  imainss 3449  funeq 3521  hbfun 3522  fununi 3549  funin 3552  hbfn 3570  2elresin 3584  zfrep6 3600  hbf 3611  hbf1 3648  f1co 3652  hbfo 3656  fof 3657  foco 3667  hbf1o 3672  f1ocnv 3686  f1ores 3688  f1oco 3692  fopab2 3808  hbiso 3877  isocnv 3881  isotr 3882  isotrALT 3883  tz7.48lem 3940  ider 4253  eqer 4255  map0 4328  ixpeq2 4339  enssdom 4364  sbthlem9 4435  mapunen 4482  zfreg 4568  zfreg2 4569  dfom3 4602  infensuc 4610  scott0 4689  ac6n 4729  ac9s 4736  dominf 4876  cdainf 4909  ltsopq 5047  1pr 5089  reclem2pr 5129  ltsosr 5175  ltsor 5233  ltadd2 5564  recgt0i 5770  ltmul1i 5777  peano2nn 5883  sup2 5998  peano2uz2 6149  zqt 6198  elioc2t 6322  elico2t 6323  elicc2t 6324  eluzp1p1t 6367  peano2uz 6379  sumsqne0 6565  nnesq 6592  recvalz 6825  cjdiv 6826  cau5i 6854  fsumser0f 6939  fsumser1f 6940  ser0cj 7003  climcmplem 7073  ivthlem6OLD 7230  ivthlem7OLD 7231  efltb 7348  reeff1o 7368  sin02gt0 7420  infxpidmlem10 7504  indistop 7590  fctop 7592  cctop 7594  retopbas 7597  blssioo 7852  ablmul 8068  sspval 8316  cosh111lem2 8630  efifolem4 8640  efifo 8644  efif1lem1 8645  efif1lem2 8646  hhcmpl 8990  chsscm 9033  chcmh 9034  shscl 9196  shunss 9252  shslej 9253  shlub 9261  pjoml3 9446  cmcmlem 9451  nonbool 9513  5oalem2 9517  3oalem2 9525  lnopco0 9844  bra11 9954  pjnmop 9986  pjnormss 10007  pj3lem1 10044  mdsldmd1 10166  hatomistic 10197  cvexch 10204  cmdmd 10251  mddmdin0 10263  cdj3lem3b 10272  symgf 10310  symggrpiOLD 10311  symggrpi 10313  fine 10348  abfi 10349  neiopne 10369  infi 10448

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