Theorem 3imtr4i 236

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
3imtr4i	|- (ch -> th)

Proof of Theorem 3imtr4i

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

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

This theorem is referenced by:  orim12i 363  pm5.18OLD 723  orbidi 815  3anim123i 1053  hbex 1353  hbor 1355  hban 1356  hbbi 1357  hb3or 1358  hb3an 1359  hbe1 1363  19.29OLD 1422  19.29r 1423  19.30 1436  19.30OLD 1437  sbimi 1537  sbequ12rOLD 1547  hbs1f 1555  hbeu1 1781  hbeu 1782  sb8eu 1783  hbmo1 1802  hbmo 1803  euan 1827  mopick2OLD 1838  2exeu 1850  2eu6 1858  hbab1 1874  hbab 1875  hbxfr 1992  hbeq 1995  hbel 1996  hbne 2103  hbnel 2104  hbral 2146  hbra1 2147  hbra2 2148  hbrex 2149  hbre1 2150  ralimi2 2165  reximOLD 2195  reximi2 2197  r19.27avOLD 2225  r19.28av 2226  r19.29OLD 2228  r19.29r 2229  ralcom2 2244  ralcom2OLD 2245  hbreu 2251  hbreu1 2252  elisset 2299  reurex 2440  hbsbc1vOLD 2465  sbcco2OLD 2469  sbcel12g 2552  sbceqdig 2554  hbss 2614  sseq1OLD 2638  sseq2 2639  rabss2 2689  rabss2OLD 2690  hbdif 2729  hbun 2758  unss1OLD 2774  hbin 2800  ssinOLD 2815  ssrinOLD 2818  undif4 2930  undif4OLD 2931  r19.2zb 2959  ralf0 2975  hbpw 3041  hbpr 3076  difprsn 3127  difprsnOLD 3128  snsspw 3149  hbuni 3183  hbuniOLD 3184  hbeqel 3195  uniin 3197  uniinOLD 3198  reucl 3213  hbint 3225  hbintOLD 3226  intss 3239  iuniin 3264  iuniinOLD 3265  iuneq1 3269  iuneq2 3273  iinssOLD 3305  iunpwss 3337  hbbr 3381  eunex 3500  exss 3516  opprc3 3543  hbopabOLD 3561  pwunss 3577  poeq2 3595  soeq2 3609  freq2 3633  trssord 3675  hbsuc 3736  eufromeq2 3829  onminex 3888  nlimsucg 3923  nlimsucgOLD 3924  hbxpOLD 4025  xpss 4056  hbrel 4073  cnveq 4135  hbcnv 4139  dmeq 4157  dmin 4165  hbrn 4198  hbrnOLD 4199  dmcoss 4211  dmcosseqOLD 4215  rncoeq 4217  resiexg 4253  hbimaOLD 4274  cotrOLD 4303  dminss 4330  imainss 4331  dfco2a 4394  dfco2aOLD 4395  funeq 4441  hbfun 4443  fununi 4481  funinOLD 4485  hbfn 4509  2elresin 4524  zfrep6 4545  hbf 4560  fco 4573  hbf1 4608  f1co 4612  hbfo 4616  fof 4617  foco 4628  hbf1o 4633  f1ocnv 4651  f1ocnvOLD 4652  f1ores 4654  f1oco 4661  fopab2 4796  hbiso 4868  hbisoOLD 4869  isocnv 4873  isotr 4874  isotrALT 4875  hbiota1 5091  iotaex 5099  reiota4 5107  tz7.48lem 5164  iderOLD 5327  eqer 5329  map0 5403  ixpeq2 5414  enssdom 5442  fiprc 5492  sbthlem9 5518  mapunen 5596  zfreg 5698  zfreg2 5699  dfom3 5737  infensuc 5745  scott0 5847  elomsubsd 5885  ac6n 5919  ac9s 5926  dominf 6052  cdainf 6087  ltsopq 6227  1pr 6269  reclem2pr 6309  ltsosr 6355  ltsor 6413  ssxr 6714  ltadd2i 6765  recgt0ii 6992  ltmul1ii 6999  peano2nn 7118  sup2 7260  peano2uz2 7413  zq 7440  irradd 7457  irrmul 7458  elioc2 7558  elico2 7559  elicc2 7560  eluzp1p1 7604  peano2uz 7616  sumsqne0i 7879  nnesqi 7912  recvalzi 8139  cjdivi 8140  cau5ii 8169  fsumser0fi 8261  fsumser1fi 8262  ser0cji 8325  climcmplem 8397  efltbi 8672  reeff1o 8691  sin02gt0 8744  infxpidmlem10 8830  fctop 8920  cctop 8922  retopbas 8925  blssioo 9191  ablmul 9439  sspval 9721  cosh111lem2 10069  efifolem4 10079  efifo 10083  efif1lem1 10084  efif1lem2 10085  symgf 10204  symggrpi 10205  fine 10213  abfi 10215  fgfil 10290  tosdir 10358  axhcompl 10500  hhcmpl 10702  chsscmi 10745  chcmhi 10746  shscli 10914  shunssi 10970  shsleji 10971  shlubi 10979  pjoml3i 11162  cmcmlem 11167  nonbooli 11231  5oalem2 11235  3oalem2 11243  lnopco0i 11566  bra11 11679  pjnmopi 11719  pjnormssi 11740  pj3lem1 11779  mdsldmd1i 11903  hatomistici 11934  cvexchi 11941  cmdmdi 11989  mddmdin0i 12003  cdj3lem3b 12012  bnj10OLD 12375  bnj48 12422  bnj111OLD 12456  bnj142 12474  bnj162OLD 12488  bnj180 12497  bnj572 12545  bnj899 12816  bnj945 12844  bnj1208 12982  bnj98 13221  bnj545 13271  bnj556 13280  bnj557 13281  bnj583 13296  bnj607 13304  bnj944 13340  bnj949 13341  bnj999 13365  bnj1067 13399  r19.30 13817  fundmpss 13836  fresin 13840  setinds 13844  elpotr 13847  dfon2lem8 13856  trcllem1 13933  poseq 13954  wfrlem5 13961  wfrlem9 13965  sltval2 13997  noreson 14001  axsltsolem1 14006  axfelem11 14041  txpss3v 14065  limitssson 14080  meran1 14235  arg-ax 14240  nxtor 14312  evpexun 14322  neiopne 14354  hbcp 14500  npincppr 14501  dstr 14516  tolat 14631  latdir 14643  ablcomgrp 14702  fprodsub 14742  trinv 14759  eqindhome 14895  cntrsetlem 14999  issubcat 15193  taralt 15211  elomsubsdOLD 15394  alexsublem4 15440  reconnlem3 15448  reconnlem4 15449  reconnlem5 15450  neibastop2lem4 15522  fnejoin2 15531  filssufil 15571  difxp 15690  hbixp1 15725  firnfi3 15743  sdc 15811  fdc 15812  fsumltisumi 15823  caushft 15851  iirev 15871  iihalf1 15872  iihalf2 15873  iimulcl 15874  sstotbnd 15936  bndss 15942  heiborlem15 15969  heiborlem16 15970  heiborlem30 15984  heiborlem35 15989  fldcrng 16152  flddmn 16206  ax10ext 16364  iotaexeu 16382  smores 16446  clatlat 16893  osumcllem11 17374

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 164

Copyright terms: Public domain