Theorem 3imtr4i 281

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  hbxfrbi  1752  nfntOLDOLD  1783  sbimi  1886  ralimi2  2949  reximi2  3010  r19.28v  3071  r19.29r  3073  r19.30  3082  elex  3212  rmoan  3406  rmoimi2  3409  sseq2  3627  rabss2  3685  n0rex  3935  undif4  4035  r19.2zb  4061  ralf0OLD  4079  difprsnss  4329  snsspw  4375  uniin  4457  iuniin  4531  iuneq1  4534  iuneq2  4537  iunpwss  4618  eunex  4859  rmorabex  4928  exss  4931  pwunss  5019  soeq2  5055  elopaelxp  5191  reliin  5240  coeq1  5279  coeq2  5280  cnveq  5296  dmeq  5324  dmin  5332  dmcoss  5385  rncoeq  5389  dminss  5547  imainss  5548  dfco2a  5635  iotaex  5868  fundif  5935  fununi  5964  fof  6115  f1ocnv  6149  foco2  6379  isocnv  6580  isotr  6586  oprabid  6677  resiexg  7102  zfrep6  7134  ovmptss  7258  dmtpos  7364  tposfn  7381  smores  7449  omopthlem1  7735  eqer  7777  eqerOLD  7778  ixpeq2  7922  enssdom  7980  fiprc  8039  sbthlem9  8078  infensuc  8138  fipwuni  8332  zfregOLD  8502  zfreg2OLD  8503  dfom3  8544  r1elss  8669  scott0  8749  fin56  9215  dominf  9267  ac6n  9307  brdom4  9352  dominfac  9395  inawina  9512  eltsk2g  9573  ltsosr  9915  ssxr  10107  recgt0ii  10929  sup2  10979  dfnn2  11033  peano2uz2  11465  eluzp1p1  11713  peano2uz  11741  zq  11794  ubmelfzo  12532  elfzlmr  12582  expclzlem  12884  wrdeq  13327  wwlktovf  13699  fsum2dlem  14501  fprod2dlem  14710  sin02gt0  14922  divalglem6  15121  qredeu  15372  isfunc  16524  xpcbas  16818  drsdirfi  16938  clatl  17116  tsrss  17223  gimcnv  17709  gsum2dlem1  18369  gsum2dlem2  18370  lmimcnv  19067  xrge0subm  19787  fctop  20808  cctop  20810  alexsubALTlem4  21854  lpbl  22308  xrge0gsumle  22636  xrge0tsms  22637  iirev  22728  iihalf1  22730  iihalf2  22732  iimulcl  22736  vitalilem1  23376  vitalilem1OLD  23377  ply1idom  23884  aacjcl  24082  aannenlem2  24084  ang180lem4  24542  lgslem3  25024  axlowdim  25841  axcontlem2  25845  usgrexmplef  26151  cusgrop  26334  rusgrpropedg  26480  spthispth  26622  cycliscrct  26694  wwlksn0  26748  nmobndseqi  27634  axhcompl-zf  27855  hhcmpl  28057  shunssi  28227  spansni  28416  pjoml3i  28445  cmcmlem  28450  nonbooli  28510  lnopco0i  28863  pjnmopi  29007  pjnormssi  29027  hatomistici  29221  cvexchi  29228  cmdmdi  29276  mddmdin0i  29290  cdj3lem3b  29299  disjin  29399  disjin2  29400  xrge0tsmsd  29785  issgon  30186  sxbrsigalem0  30333  eulerpartlemgs2  30442  ballotlem2  30550  ballotth  30599  bnj945  30844  bnj556  30970  bnj557  30971  bnj607  30986  bnj864  30992  bnj969  31016  bnj999  31027  bnj1398  31102  elpotr  31686  dfon2lem8  31695  sltval2  31809  txpss3v  31985  meran1  32410  arg-ax  32415  bj-nfalt  32702  bj-eunex  32799  poimirlem25  33434  poimirlem30  33439  bndss  33585  fldcrng  33803  flddmn  33857  xrnss3v  34135  prter1  34164  mzpclall  37290  setindtrs  37592  dgraalem  37715  ifpimim  37854  inintabss  37884  refimssco  37913  cotrintab  37921  intimass  37946  psshepw  38082  nzin  38517  axc11next  38607  iotaexeu  38619  hbexgVD  39142  reuan  41180  aovpcov0  41270  aov0ov0  41273  enege  41558  onego  41559  gbogbow  41644  spr0el  41732  sprsymrelf  41745  mhmismgmhm  41806  sgrpplusgaopALT  41831  rhmisrnghm  41920  srhmsubclem1  42073  rhmsubcALTVlem3  42106  eluz2cnn0n1  42301  regt1loggt0  42330  rege1logbrege0  42352  rege1logbzge0  42353  relogbmulbexp  42355