Theorem 3imtr4i 284

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  hbxfrbi  1868  sbimi  2017  nexmo  2552  moimi  2557  eu6im  2593  ralimi2  3131  reximi2  3191  r19.28v  3257  r19.29r  3259  r19.30  3268  elex  3414  rmoan  3620  rmoimi2  3623  sseq2  3846  rabss2  3906  n0rex  4163  undif4  4259  r19.2zb  4284  difprsnss  4563  snsspw  4606  uniin  4695  iuniin  4766  iuneq1  4769  iuneq2  4772  iunpwss  4854  eunex  5103  eunexOLD  5104  rmorabex  5162  exss  5165  pwunss  5258  soeq2  5297  elopaelxp  5441  reliin  5490  coeq1  5527  coeq2  5528  cnveq  5543  dmeq  5571  dmin  5579  dmcoss  5633  rncoeq  5637  dminss  5803  imainss  5804  dfco2a  5891  iotaex  6118  fundif  6185  fununi  6211  fof  6368  f1ocnv  6405  foco2  6645  isocnv  6854  isotr  6860  oprabid  6955  zfrep6  7415  ovmptss  7541  dmtpos  7648  tposfn  7665  smores  7734  omopthlem1  8021  eqer  8063  ixpeq2  8210  enssdom  8268  fiprc  8329  sbthlem9  8368  infensuc  8428  fipwuni  8622  dfom3  8843  r1elss  8968  scott0  9048  fin56  9552  dominf  9604  ac6n  9644  brdom4  9689  dominfac  9732  inawina  9849  eltsk2g  9910  ltsosr  10253  ssxr  10448  recgt0ii  11285  sup2  11337  dfnn2  11393  peano2uz2  11821  eluzp1p1  12022  peano2uz  12051  zqOLD  12106  ubmelfzo  12856  elfzlmr  12905  expclzlem  13206  wrdeq  13628  wwlktovf  14112  fsum2dlem  14910  fprod2dlem  15117  sin02gt0  15328  divalglem6  15532  qredeu  15781  isfunc  16913  xpcbas  17208  drsdirfi  17328  clatl  17506  tsrss  17613  gimcnv  18097  gsum2dlem1  18759  gsum2dlem2  18760  lmimcnv  19466  xrge0subm  20187  fctop  21220  cctop  21222  alexsubALTlem4  22266  lpbl  22720  xrge0gsumle  23048  xrge0tsms  23049  iirev  23140  iihalf1  23142  iihalf2  23144  iimulcl  23148  vitalilem1  23816  ply1idom  24325  aacjcl  24523  aannenlem2  24525  ang180lem4  24994  lgslem3  25480  tgjustf  25828  axlowdim  26314  axcontlem2  26318  usgrexmplef  26610  cusgrop  26790  rusgrpropedg  26936  spthispth  27082  cycliscrct  27155  wwlksn0  27216  clwwlkccat  27374  clwwlkn  27419  clwwlknonccat  27502  numclwwlk1  27788  nmobndseqi  28210  axhcompl-zf  28431  hhcmpl  28633  shunssi  28803  spansni  28992  pjoml3i  29021  cmcmlem  29026  nonbooli  29086  lnopco0i  29439  pjnmopi  29583  pjnormssi  29603  hatomistici  29797  cvexchi  29804  cmdmdi  29852  mddmdin0i  29866  cdj3lem3b  29875  disjin  29966  disjin2  29967  xrge0tsmsd  30351  issgon  30788  sxbrsigalem0  30935  eulerpartlemgs2  31044  ballotlem2  31153  ballotth  31202  bnj945  31447  bnj556  31573  bnj557  31574  bnj607  31589  bnj864  31595  bnj969  31619  bnj999  31630  bnj1398  31705  elpotr  32278  dfon2lem8  32287  sltval2  32402  txpss3v  32578  meran1  32997  arg-ax  33002  bj-nfalt  33294  bj-eunex  33379  wl-cbvmotv  33894  poimirlem25  34065  poimirlem30  34070  bndss  34214  fldcrng  34432  flddmn  34486  xrnss3v  34767  redss3  35002  redpim3  35004  prter1  35038  mzpclall  38260  setindtrs  38561  dgraalem  38684  ifpimim  38822  inintabss  38851  refimssco  38880  cotrintab  38888  intimass  38913  psshepw  39048  nzin  39483  axc11next  39572  iotaexeu  39584  hbexgVD  40085  reuan  42148  aovpcov0  42241  aov0ov0  42244  spr0el  42431  sprsymrelf  42444  enege  42593  onego  42594  gbogbow  42679  mhmismgmhm  42831  sgrpplusgaopALT  42856  rhmisrnghm  42945  srhmsubclem1  43098  rhmsubcALTVlem3  43131  eluz2cnn0n1  43326  regt1loggt0  43355  rege1logbrege0  43377  rege1logbzge0  43378  relogbmulbexp  43380