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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  hbxfrbi  1824  excomimw  2042  nexmo  2540  moimi  2544  eu6im  2574  ralimi2  3077  reximi2  3078  rexbiOLD  3104  rabid2im  3468  elexOLD  3501  rmoan  3744  rmoimi2  3748  reuan  3895  sstr2  3989  rabss2  4077  n0rex  4356  undif4  4466  r19.2zb  4495  rzal  4508  difprsnss  4798  snsspw  4843  uniin  4930  iuniin  5003  iuneq1  5007  iuneq2  5010  iunpwss  5106  axrep6  5287  axrep6OLD  5288  eunex  5389  rmorabex  5464  exss  5467  soeq2  5613  elopaelxpOLD  5775  reliin  5826  coeq1  5867  coeq2  5868  cnveq  5883  dmeq  5913  dmin  5921  dmcoss  5984  rncoeq  5989  dminss  6172  imainss  6173  dfco2a  6265  iotaexOLD  6540  fundif  6614  fununi  6640  fof  6819  f1ocnv  6859  foco2  7128  isocnv  7351  isotr  7357  oprabidw  7463  oprabid  7464  zfrep6  7980  ovmptss  8119  dmtpos  8264  tposfn  8281  smores  8393  omopthlem1  8698  brinxper  8775  eqer  8782  fsetsspwxp  8894  ixpeq2  8952  enssdom  9018  fiprc  9086  sbthlem9  9132  infensuc  9196  fipwuni  9467  dfom3  9688  ttrcltr  9757  r1elss  9847  scott0  9927  fin56  10434  dominf  10486  ac6n  10526  brdom4  10571  dominfac  10614  inawina  10731  eltsk2g  10792  ltsosr  11135  ssxr  11331  recgt0ii  12175  sup2  12225  dfnn2  12280  peano2uz2  12708  eluzp1p1  12907  peano2uz  12944  ubmelfzo  13770  elfzlmr  13821  expclzlem  14125  wrdeq  14575  wwlktovf  14996  fsum2dlem  15807  fprod2dlem  16017  sin02gt0  16229  divalglem6  16436  qredeu  16696  isfunc  17910  xpcbas  18224  drsdirfi  18352  clatl  18554  tsrss  18635  mhmismgmhm  18805  smndex1mgm  18921  gimcnv  19286  gsum2dlem1  19989  gsum2dlem2  19990  rhmisrnghm  20481  subrngrng  20551  srhmsubclem1  20678  fldidom  20772  lmimcnv  21067  xrge0subm  21426  fctop  23012  cctop  23014  alexsubALTlem4  24059  lpbl  24517  xrge0gsumle  24856  xrge0tsms  24857  iirev  24957  iihalf1  24959  iihalf2  24962  iimulcl  24967  vitalilem1  25644  ply1idom  26165  aacjcl  26370  aannenlem2  26372  ang180lem4  26856  lgslem3  27344  sltval2  27702  madef  27896  lrrecfr  27977  norecdiv  28217  elons2  28282  dfn0s2  28337  nnaddscl  28350  nnmulscl  28351  znegscl  28379  uzsind  28392  renegscl  28431  readdscl  28432  remulscl  28435  tgjustf  28482  axlowdim  28977  axcontlem2  28981  usgrexmplef  29277  cusgrop  29456  rusgrpropedg  29603  spthispth  29745  pthdifv  29751  cycliscrct  29820  wwlksn0  29884  clwwlkccat  30010  clwwlkn  30046  clwwlknonccat  30116  numclwwlk1  30381  nmobndseqi  30799  axhcompl-zf  31018  hhcmpl  31220  shunssi  31388  spansni  31577  pjoml3i  31606  cmcmlem  31611  nonbooli  31671  lnopco0i  32024  pjnmopi  32168  pjnormssi  32188  hatomistici  32382  cvexchi  32389  cmdmdi  32437  mddmdin0i  32451  cdj3lem3b  32460  rmoun  32514  disjin  32600  disjin2  32601  xrge0tsmsd  33066  issgon  34125  sxbrsigalem0  34274  eulerpartlemgs2  34383  ballotlem2  34492  ballotth  34541  bnj945  34788  bnj556  34915  bnj557  34916  bnj607  34931  bnj864  34937  bnj969  34961  bnj999  34973  bnj1398  35049  wevgblacfn  35115  elpotr  35783  dfon2lem8  35792  txpss3v  35880  meran1  36413  arg-ax  36418  bj-nfalt  36713  bj-imdirco  37192  difunieq  37376  pibt1  37418  wl-cbvmotv  37515  poimirlem25  37653  poimirlem30  37658  bndss  37794  fldcrngo  38012  flddmn  38066  xrnss3v  38374  trressn  38447  redundss3  38630  redundpim3  38632  eldisjim  38786  eldisjim2  38787  eldisjn0el  38808  partim  38810  mainer  38836  prter1  38881  sn-sup2  42506  rimcnv  42532  fimgmcyclem  42548  mzpclall  42743  setindtrs  43042  dgraalem  43162  oneptri  43274  ifpimim  43527  inintabss  43596  refimssco  43625  cotrintab  43632  intimass  43672  psshepw  43806  nzin  44342  axc11next  44430  iotaexeu  44442  hbexgVD  44931  wfaxrep  45016  wfaxsep  45017  wfaxpow  45019  wfaxpr  45020  wfac8prim  45024  absnsb  47044  aovpcov0  47207  aov0ov0  47210  ichan  47447  ichal  47458  spr0el  47474  sprsymrelf  47487  enege  47637  onego  47638  gbogbow  47748  gpgvtxedg0  48026  gpgvtxedg1  48027  sgrpplusgaopALT  48116  rhmsubcALTVlem3  48204  eluz2cnn0n1  48433  regt1loggt0  48462  rege1logbrege0  48484  rege1logbzge0  48485  relogbmulbexp  48487