Theorem 3imtr4i 292

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 216	. 2 ⊢ (𝜒 → 𝜓)
4		3imtr4.3	. 2 ⊢ (𝜃 ↔ 𝜓)
5	3, 4	sylibr 233	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  hbxfrbi  1828  nexmo  2536  moimi  2540  eu6im  2570  ralimi2  3079  reximi2  3080  rexbiOLD  3106  elex  3493  rmoan  3736  rmoimi2  3740  reuan  3891  sseq2  4009  rabss2  4076  n0rex  4355  undif4  4467  r19.2zb  4496  rzal  4509  difprsnss  4803  snsspw  4846  uniin  4936  iuniin  5010  iuneq1  5014  iuneq2  5017  iunpwss  5111  axrep6  5293  eunex  5389  rmorabex  5461  exss  5464  soeq2  5611  elopaelxpOLD  5767  reliin  5818  coeq1  5858  coeq2  5859  cnveq  5874  dmeq  5904  dmin  5912  dmcoss  5971  rncoeq  5975  dminss  6153  imainss  6154  dfco2a  6246  iotaexOLD  6524  fundif  6598  fununi  6624  fof  6806  f1ocnv  6846  foco2  7109  isocnv  7327  isotr  7333  oprabidw  7440  oprabid  7441  zfrep6  7941  ovmptss  8079  dmtpos  8223  tposfn  8240  smores  8352  omopthlem1  8658  eqer  8738  fsetsspwxp  8847  ixpeq2  8905  enssdom  8973  fiprc  9045  sbthlem9  9091  infensuc  9155  fipwuni  9421  dfom3  9642  ttrcltr  9711  r1elss  9801  scott0  9881  fin56  10388  dominf  10440  ac6n  10480  brdom4  10525  dominfac  10568  inawina  10685  eltsk2g  10746  ltsosr  11089  ssxr  11283  recgt0ii  12120  sup2  12170  dfnn2  12225  peano2uz2  12650  eluzp1p1  12850  peano2uz  12885  ubmelfzo  13697  elfzlmr  13746  expclzlem  14049  wrdeq  14486  wwlktovf  14907  fsum2dlem  15716  fprod2dlem  15924  sin02gt0  16135  divalglem6  16341  qredeu  16595  isfunc  17814  xpcbas  18130  drsdirfi  18258  clatl  18461  tsrss  18542  smndex1mgm  18788  gimcnv  19141  gsum2dlem1  19838  gsum2dlem2  19839  lmimcnv  20678  fldidom  20923  xrge0subm  20986  fctop  22507  cctop  22509  alexsubALTlem4  23554  lpbl  24012  xrge0gsumle  24349  xrge0tsms  24350  iirev  24445  iihalf1  24447  iihalf2  24449  iimulcl  24453  vitalilem1  25125  ply1idom  25642  aacjcl  25840  aannenlem2  25842  ang180lem4  26317  lgslem3  26802  sltval2  27159  madef  27352  lrrecfr  27429  norecdiv  27641  elons2  27688  dfn0s2  27705  n0sind  27706  tgjustf  27755  axlowdim  28250  axcontlem2  28254  usgrexmplef  28547  cusgrop  28726  rusgrpropedg  28872  spthispth  29014  cycliscrct  29087  wwlksn0  29148  clwwlkccat  29274  clwwlkn  29310  clwwlknonccat  29380  numclwwlk1  29645  nmobndseqi  30063  axhcompl-zf  30282  hhcmpl  30484  shunssi  30652  spansni  30841  pjoml3i  30870  cmcmlem  30875  nonbooli  30935  lnopco0i  31288  pjnmopi  31432  pjnormssi  31452  hatomistici  31646  cvexchi  31653  cmdmdi  31701  mddmdin0i  31715  cdj3lem3b  31724  rmoun  31765  disjin  31848  disjin2  31849  xrge0tsmsd  32240  issgon  33152  sxbrsigalem0  33301  eulerpartlemgs2  33410  ballotlem2  33518  ballotth  33567  bnj945  33815  bnj556  33942  bnj557  33943  bnj607  33958  bnj864  33964  bnj969  33988  bnj999  34000  bnj1398  34076  elpotr  34784  dfon2lem8  34793  txpss3v  34881  meran1  35344  arg-ax  35349  bj-nfalt  35637  bj-imdirco  36119  difunieq  36303  pibt1  36345  wl-cbvmotv  36430  poimirlem25  36561  poimirlem30  36566  bndss  36702  fldcrngo  36920  flddmn  36974  xrnss3v  37290  trressn  37363  redundss3  37546  redundpim3  37548  eldisjim  37702  eldisjim2  37703  eldisjn0el  37724  partim  37726  mainer  37752  prter1  37797  rimcnv  41140  sn-sup2  41390  mzpclall  41513  setindtrs  41812  dgraalem  41935  oneptri  42054  ifpimim  42308  inintabss  42377  refimssco  42406  cotrintab  42413  intimass  42453  psshepw  42587  nzin  43125  axc11next  43213  iotaexeu  43225  hbexgVD  43715  absnsb  45785  aovpcov0  45946  aov0ov0  45949  ichan  46171  ichal  46182  spr0el  46198  sprsymrelf  46211  enege  46361  onego  46362  gbogbow  46472  mhmismgmhm  46624  sgrpplusgaopALT  46653  rhmisrnghm  46771  subrngrng  46777  srhmsubclem1  47019  rhmsubcALTVlem3  47052  eluz2cnn0n1  47240  regt1loggt0  47270  rege1logbrege0  47292  rege1logbzge0  47293  relogbmulbexp  47295