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  1819  nexmo  2527  moimi  2531  eu6im  2561  ralimi2  3070  reximi2  3071  rexbiOLD  3097  elex  3485  rmoan  3727  rmoimi2  3731  reuan  3882  sseq2  4000  rabss2  4067  n0rex  4346  undif4  4458  r19.2zb  4487  rzal  4500  difprsnss  4794  snsspw  4837  uniin  4925  iuniin  4999  iuneq1  5003  iuneq2  5006  iunpwss  5100  axrep6  5282  eunex  5378  rmorabex  5450  exss  5453  soeq2  5600  elopaelxpOLD  5756  reliin  5807  coeq1  5847  coeq2  5848  cnveq  5863  dmeq  5893  dmin  5901  dmcoss  5960  rncoeq  5964  dminss  6142  imainss  6143  dfco2a  6235  iotaexOLD  6513  fundif  6587  fununi  6613  fof  6795  f1ocnv  6835  foco2  7100  isocnv  7319  isotr  7325  oprabidw  7432  oprabid  7433  zfrep6  7934  ovmptss  8073  dmtpos  8218  tposfn  8235  smores  8347  omopthlem1  8653  eqer  8733  fsetsspwxp  8842  ixpeq2  8900  enssdom  8968  fiprc  9040  sbthlem9  9086  infensuc  9150  fipwuni  9416  dfom3  9637  ttrcltr  9706  r1elss  9796  scott0  9876  fin56  10383  dominf  10435  ac6n  10475  brdom4  10520  dominfac  10563  inawina  10680  eltsk2g  10741  ltsosr  11084  ssxr  11279  recgt0ii  12116  sup2  12166  dfnn2  12221  peano2uz2  12646  eluzp1p1  12846  peano2uz  12881  ubmelfzo  13693  elfzlmr  13742  expclzlem  14045  wrdeq  14482  wwlktovf  14903  fsum2dlem  15712  fprod2dlem  15920  sin02gt0  16131  divalglem6  16337  qredeu  16591  isfunc  17812  xpcbas  18131  drsdirfi  18259  clatl  18462  tsrss  18543  mhmismgmhm  18710  smndex1mgm  18821  gimcnv  19181  gsum2dlem1  19879  gsum2dlem2  19880  rhmisrnghm  20371  subrngrng  20439  srhmsubclem1  20562  lmimcnv  20904  fldidom  21206  xrge0subm  21269  fctop  22828  cctop  22830  alexsubALTlem4  23875  lpbl  24333  xrge0gsumle  24670  xrge0tsms  24671  iirev  24771  iihalf1  24773  iihalf2  24776  iimulcl  24781  vitalilem1  25458  ply1idom  25981  aacjcl  26180  aannenlem2  26182  ang180lem4  26659  lgslem3  27147  sltval2  27504  madef  27698  lrrecfr  27775  norecdiv  28005  elons2  28066  dfn0s2  28087  n0sind  28088  nnaddscl  28098  nnmulscl  28099  renegscl  28108  readdscl  28109  remulscl  28112  tgjustf  28159  axlowdim  28654  axcontlem2  28658  usgrexmplef  28951  cusgrop  29130  rusgrpropedg  29276  spthispth  29418  cycliscrct  29491  wwlksn0  29552  clwwlkccat  29678  clwwlkn  29714  clwwlknonccat  29784  numclwwlk1  30049  nmobndseqi  30467  axhcompl-zf  30686  hhcmpl  30888  shunssi  31056  spansni  31245  pjoml3i  31274  cmcmlem  31279  nonbooli  31339  lnopco0i  31692  pjnmopi  31836  pjnormssi  31856  hatomistici  32050  cvexchi  32057  cmdmdi  32105  mddmdin0i  32119  cdj3lem3b  32128  rmoun  32169  disjin  32252  disjin2  32253  xrge0tsmsd  32643  issgon  33576  sxbrsigalem0  33725  eulerpartlemgs2  33834  ballotlem2  33942  ballotth  33991  bnj945  34239  bnj556  34366  bnj557  34367  bnj607  34382  bnj864  34388  bnj969  34412  bnj999  34424  bnj1398  34500  elpotr  35214  dfon2lem8  35223  txpss3v  35311  meran1  35752  arg-ax  35757  bj-nfalt  36045  bj-imdirco  36527  difunieq  36711  pibt1  36753  wl-cbvmotv  36838  poimirlem25  36969  poimirlem30  36974  bndss  37110  fldcrngo  37328  flddmn  37382  xrnss3v  37698  trressn  37771  redundss3  37954  redundpim3  37956  eldisjim  38110  eldisjim2  38111  eldisjn0el  38132  partim  38134  mainer  38160  prter1  38205  rimcnv  41549  sn-sup2  41797  mzpclall  41920  setindtrs  42219  dgraalem  42342  oneptri  42461  ifpimim  42715  inintabss  42784  refimssco  42813  cotrintab  42820  intimass  42860  psshepw  42994  nzin  43532  axc11next  43620  iotaexeu  43632  hbexgVD  44122  absnsb  46188  aovpcov0  46349  aov0ov0  46352  ichan  46574  ichal  46585  spr0el  46601  sprsymrelf  46614  enege  46764  onego  46765  gbogbow  46875  sgrpplusgaopALT  47024  rhmsubcALTVlem3  47112  eluz2cnn0n1  47346  regt1loggt0  47376  rege1logbrege0  47398  rege1logbzge0  47399  relogbmulbexp  47401