Theorem 3imtr4i 295

Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
3imtr4.1	⊢ (𝜑 → 𝜓)
3imtr4.2	⊢ (𝜒 ↔ 𝜑)
3imtr4.3	⊢ (𝜃 ↔ 𝜓)

Assertion

Ref	Expression
3imtr4i	⊢ (𝜒 → 𝜃)

Proof of Theorem 3imtr4i

Step	Hyp	Ref	Expression
1		3imtr4.2	. . 3 ⊢ (𝜒 ↔ 𝜑)
2		3imtr4.1	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	sylbi 220	. 2 ⊢ (𝜒 → 𝜓)
4		3imtr4.3	. 2 ⊢ (𝜃 ↔ 𝜓)
5	3, 4	sylibr 237	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209

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

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  hbxfrbi  1855  excomimw  2074  nexmo  2569  eu6im  2603  ralimi2  3097  reximi2  3098  rabid2im  3448  rmoan  3702  rmoimi2  3706  reuan  3850  sstr2  3944  rabss2OLD  4032  n0rex  4312  undif4  4427  rzal  4455  difprsnss  4767  snsspw  4809  uniinOLD  4897  iuniin  4969  iuneq1  4973  iuneq2  4976  iunpwss  5073  axrep6  5247  axrep6OLD  5248  eunex  5361  rmorabex  5441  exss  5444  soeq2  5591  reliin  5804  coeq1  5843  coeq2  5844  cnveq  5859  dmeq  5893  dmin  5901  dmcoss  5965  dmcossOLD  5966  rncoeq  5971  dminss  6150  imainss  6151  dfco2a  6247  fundif  6585  fununi  6611  fof  6792  f1ocnv  6833  foco2  7104  isocnv  7328  isotr  7334  oprabidw  7441  oprabid  7442  zfrep6OLD  7948  ovmptss  8084  dmtpos  8230  tposfn  8247  smores  8335  omopthlem1  8641  brinxper  8720  eqer  8727  fsetsspwxp  8846  ixpeq2  8905  enssdomOLD  8970  fiprc  9037  sbthlem9  9079  infensuc  9139  fipwuni  9382  dfom3  9612  ttrcltr  9681  r1elss  9774  scott0  9856  fin56  10372  dominf  10424  ac6n  10464  brdom4  10509  dominfac  10553  inawina  10670  eltsk2g  10731  ltsosr  11074  ssxr  11274  recgt0ii  12116  sup2  12166  dfnn2  12241  peano2uz2  12679  eluzp1p1  12885  peano2uz  12920  ubmelfzo  13755  elfzlmr  13807  expclzlem  14115  wrdeq  14569  wwlktovf  14989  fsum2dlem  15817  fprod2dlem  16030  sin02gt0  16243  divalglem6  16451  qredeu  16711  isfunc  17916  xpcbas  18229  drsdirfi  18356  clatl  18559  tsrss  18640  mhmismgmhm  18844  smndex1mgm  18964  gimcnv  19332  gsum2dlem1  20035  gsum2dlem2  20036  rhmisrnghm  20559  rimcnv  20565  subrngrng  20649  srhmsubclem1  20776  fldidom  20875  lmimcnv  21188  xrge0subm  21593  fctop  23161  cctop  23163  alexsubALTlem4  24207  lpbl  24660  xrge0gsumle  24991  xrge0tsms  24992  iirev  25088  iihalf1  25090  iihalf2  25092  iimulcl  25096  vitalilem1  25767  ply1idom  26282  aacjcl  26490  aannenlem2  26492  ang180lem4  26977  lgslem3  27463  ltsval2  27820  madef  28029  lrrecfr  28136  norecdiv  28383  elons2  28451  dfn0s2  28525  nnaddscl  28539  nnmulscl  28540  znegscl  28585  uzsind  28598  zsoring  28602  z12negscl  28671  renegscl  28691  readdscl  28692  remulscl  28695  tgjustf  28742  axlowdim  29311  axcontlem2  29315  usgrexmplef  29609  cusgrop  29788  rusgrpropedg  29934  spthispth  30073  pthdifv  30079  cycliscrct  30148  wwlksn0  30212  clwwlkccat  30341  clwwlkn  30377  clwwlknonccat  30447  numclwwlk1  30712  nmobndseqi  31131  axhcompl-zf  31350  hhcmpl  31552  shunssi  31720  spansni  31909  pjoml3i  31938  cmcmlem  31943  nonbooli  32003  lnopco0i  32356  pjnmopi  32500  pjnormssi  32520  hatomistici  32714  cvexchi  32721  cmdmdi  32769  mddmdin0i  32783  cdj3lem3b  32792  rmoun  32840  disjin  32931  disjin2  32932  xrge0tsmsd  33393  issgon  34513  sxbrsigalem0  34661  eulerpartlemgs2  34770  ballotlem2  34879  ballotth  34928  bnj945  35162  bnj556  35288  bnj557  35289  bnj607  35304  bnj864  35310  bnj969  35334  bnj999  35346  bnj1398  35422  kardexen  35576  wevgblacfn  35595  elpotr  36271  dfon2lem8  36280  txpss3v  36368  meran1  36942  arg-ax  36947  bj-sbcex  37293  bj-nfalt  37358  bj-imdirco  37854  difunieq  38040  pibt1  38082  wl-cbvmotv  38188  poimirlem25  38316  poimirlem30  38321  bndss  38457  fldcrngo  38675  flddmn  38729  xrnss3v  39050  trressn  39204  redundss3  39381  redundpim3  39383  eldisjim  39556  eldisjim2  39557  eldisjn0el  39578  partim  39580  mainer  39617  prter1  39673  sn-sup2  43285  fimgmcyclem  43321  mzpclall  43478  setindtrs  43772  dgraalem  43892  oneptri  44004  ifpimim  44255  inintabss  44324  refimssco  44353  cotrintab  44360  intimass  44400  psshepw  44534  nzin  45048  axc11next  45136  iotaexeu  45148  hbexgVD  45634  orbitclmpt  45687  wfaxrep  45723  wfaxsep  45724  wfaxpow  45726  wfaxpr  45727  wfac8prim  45731  permaxinf2lem  45741  absnsb  47784  aovpcov0  47947  aov0ov0  47950  muldvdsfacgt  48143  ichan  48224  ichal  48235  spr0el  48251  sprsymrelf  48264  enege  48430  onego  48431  gbogbow  48541  gpgvtxedg0  48848  gpgvtxedg1  48849  gpgprismgr4cycllem10  48889  sgrpplusgaopALT  48980  rhmsubcALTVlem3  49068  eluz2cnn0n1  49311  regt1loggt0  49336  rege1logbrege0  49358  rege1logbzge0  49359  relogbmulbexp  49361  islan2  50424  alseuals  50622  ralseurals  50623