Theorem 3imtr4i 294

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  norassOLD  1530  hbxfrbi  1821  sbimiOLD  2511  sbimiALT  2573  nexmo  2619  moimi  2623  eu6im  2656  ralimi2  3157  r19.28vOLD  3187  reximi2  3244  r19.29rOLD  3256  r19.30OLD  3339  elisset  3505  elex  3512  rmoan  3729  rmoimi2  3733  reuan  3879  sseq2  3992  rabss2  4053  n0rex  4313  undif4  4415  r19.2zb  4440  difprsnss  4725  snsspw  4768  uniin  4851  iuniin  4923  iuneq1  4927  iuneq2  4930  iunpwss  5021  axrep6  5189  eunex  5282  rmorabex  5344  exss  5347  pwunssOLD  5448  soeq2  5489  elopaelxp  5635  reliin  5684  coeq1  5722  coeq2  5723  cnveq  5738  dmeq  5766  dmin  5774  dmcoss  5836  rncoeq  5840  dminss  6004  imainss  6005  dfco2a  6093  iotaex  6329  fundif  6397  fununi  6423  fof  6584  f1ocnv  6621  foco2  6867  isocnv  7077  isotr  7083  oprabidw  7181  oprabid  7182  zfrep6  7650  ovmptss  7782  dmtpos  7898  tposfn  7915  smores  7983  omopthlem1  8276  eqer  8318  ixpeq2  8469  enssdom  8528  fiprc  8589  sbthlem9  8629  infensuc  8689  fipwuni  8884  dfom3  9104  r1elss  9229  scott0  9309  fin56  9809  dominf  9861  ac6n  9901  brdom4  9946  dominfac  9989  inawina  10106  eltsk2g  10167  ltsosr  10510  ssxr  10704  recgt0ii  11540  sup2  11591  dfnn2  11645  peano2uz2  12064  eluzp1p1  12264  peano2uz  12295  ubmelfzo  13096  elfzlmr  13145  expclzlem  13447  wrdeq  13880  wwlktovf  14314  fsum2dlem  15119  fprod2dlem  15328  sin02gt0  15539  divalglem6  15743  qredeu  15996  isfunc  17128  xpcbas  17422  drsdirfi  17542  clatl  17720  tsrss  17827  smndex1mgm  18066  gimcnv  18401  gsum2dlem1  19084  gsum2dlem2  19085  lmimcnv  19833  xrge0subm  20580  fctop  21606  cctop  21608  alexsubALTlem4  22652  lpbl  23107  xrge0gsumle  23435  xrge0tsms  23436  iirev  23527  iihalf1  23529  iihalf2  23531  iimulcl  23535  vitalilem1  24203  ply1idom  24712  aacjcl  24910  aannenlem2  24912  ang180lem4  25384  lgslem3  25869  tgjustf  26253  axlowdim  26741  axcontlem2  26745  usgrexmplef  27035  cusgrop  27214  rusgrpropedg  27360  spthispth  27501  cycliscrct  27574  wwlksn0  27635  clwwlkccat  27762  clwwlkn  27798  clwwlknonccat  27869  numclwwlk1  28134  nmobndseqi  28550  axhcompl-zf  28769  hhcmpl  28971  shunssi  29139  spansni  29328  pjoml3i  29357  cmcmlem  29362  nonbooli  29422  lnopco0i  29775  pjnmopi  29919  pjnormssi  29939  hatomistici  30133  cvexchi  30140  cmdmdi  30188  mddmdin0i  30202  cdj3lem3b  30211  rmoun  30252  disjin  30330  disjin2  30331  xrge0tsmsd  30687  issgon  31377  sxbrsigalem0  31524  eulerpartlemgs2  31633  ballotlem2  31741  ballotth  31790  bnj945  32040  bnj556  32167  bnj557  32168  bnj607  32183  bnj864  32189  bnj969  32213  bnj999  32225  bnj1398  32301  elpotr  33021  dfon2lem8  33030  sltval2  33158  txpss3v  33334  meran1  33754  arg-ax  33759  bj-nfalt  34040  difunieq  34649  pibt1  34691  wl-cbvmotv  34747  poimirlem25  34911  poimirlem30  34916  bndss  35058  fldcrng  35276  flddmn  35330  xrnss3v  35618  redundss3  35857  redundpim3  35859  prter1  36009  mzpclall  39317  setindtrs  39615  dgraalem  39738  ifpimim  39868  inintabss  39931  refimssco  39960  cotrintab  39967  intimass  39992  psshepw  40127  nzin  40643  axc11next  40731  iotaexeu  40743  hbexgVD  41233  absnsb  43256  aovpcov0  43383  aov0ov0  43386  ichal  43621  ichan  43624  spr0el  43638  sprsymrelf  43651  enege  43804  onego  43805  gbogbow  43915  mhmismgmhm  44067  sgrpplusgaopALT  44096  rhmisrnghm  44185  srhmsubclem1  44338  rhmsubcALTVlem3  44371  eluz2cnn0n1  44560  regt1loggt0  44590  rege1logbrege0  44612  rege1logbzge0  44613  relogbmulbexp  44615