Theorem 3imtr4i 293

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  hbxfrbi  1832  excomimw  2051  nexmo  2545  eu6im  2579  ralimi2  3071  reximi2  3072  rabid2im  3423  rmoan  3680  rmoimi2  3684  reuan  3828  sstr2  3922  rabss2OLD  4009  n0rex  4285  undif4  4395  rzal  4422  difprsnss  4732  snsspw  4775  uniin  4862  iuniin  4934  iuneq1  4938  iuneq2  4941  iunpwss  5036  axrep6  5208  axrep6OLD  5209  eunex  5319  rmorabex  5399  exss  5402  soeq2  5548  reliin  5760  coeq1  5799  coeq2  5800  cnveq  5815  dmeq  5845  dmin  5853  dmcoss  5917  dmcossOLD  5918  rncoeq  5924  dminss  6104  imainss  6105  dfco2a  6197  fundif  6534  fununi  6560  fof  6739  f1ocnv  6779  foco2  7050  isocnv  7274  isotr  7280  oprabidw  7387  oprabid  7388  zfrep6OLD  7897  ovmptss  8032  dmtpos  8178  tposfn  8195  smores  8282  omopthlem1  8585  brinxper  8663  eqer  8670  fsetsspwxp  8790  ixpeq2  8849  enssdomOLD  8914  fiprc  8981  sbthlem9  9023  infensuc  9083  fipwuni  9329  dfom3  9559  ttrcltr  9628  r1elss  9721  scott0  9801  fin56  10306  dominf  10358  ac6n  10398  brdom4  10443  dominfac  10487  inawina  10604  eltsk2g  10665  ltsosr  11008  ssxr  11206  recgt0ii  12053  sup2  12103  dfnn2  12178  peano2uz2  12608  eluzp1p1  12807  peano2uz  12842  ubmelfzo  13676  elfzlmr  13728  expclzlem  14036  wrdeq  14489  wwlktovf  14909  fsum2dlem  15723  fprod2dlem  15936  sin02gt0  16150  divalglem6  16358  qredeu  16618  isfunc  17822  xpcbas  18135  drsdirfi  18262  clatl  18465  tsrss  18546  mhmismgmhm  18750  smndex1mgm  18869  gimcnv  19233  gsum2dlem1  19936  gsum2dlem2  19937  rhmisrnghm  20451  rimcnv  20456  subrngrng  20522  srhmsubclem1  20649  fldidom  20743  lmimcnv  21057  xrge0subm  21418  fctop  22987  cctop  22989  alexsubALTlem4  24033  lpbl  24486  xrge0gsumle  24817  xrge0tsms  24818  iirev  24914  iihalf1  24916  iihalf2  24918  iimulcl  24922  vitalilem1  25593  ply1idom  26108  aacjcl  26311  aannenlem2  26313  ang180lem4  26794  lgslem3  27280  ltsval2  27638  madef  27846  lrrecfr  27953  norecdiv  28200  elons2  28268  dfn0s2  28342  nnaddscl  28356  nnmulscl  28357  znegscl  28402  uzsind  28415  zsoring  28419  z12negscl  28488  renegscl  28508  readdscl  28509  remulscl  28512  tgjustf  28559  axlowdim  29048  axcontlem2  29052  usgrexmplef  29346  cusgrop  29525  rusgrpropedg  29671  spthispth  29810  pthdifv  29816  cycliscrct  29885  wwlksn0  29949  clwwlkccat  30078  clwwlkn  30114  clwwlknonccat  30184  numclwwlk1  30449  nmobndseqi  30868  axhcompl-zf  31087  hhcmpl  31289  shunssi  31457  spansni  31646  pjoml3i  31675  cmcmlem  31680  nonbooli  31740  lnopco0i  32093  pjnmopi  32237  pjnormssi  32257  hatomistici  32451  cvexchi  32458  cmdmdi  32506  mddmdin0i  32520  cdj3lem3b  32529  rmoun  32581  disjin  32675  disjin2  32676  xrge0tsmsd  33154  issgon  34307  sxbrsigalem0  34455  eulerpartlemgs2  34564  ballotlem2  34673  ballotth  34722  bnj945  34956  bnj556  35082  bnj557  35083  bnj607  35098  bnj864  35104  bnj969  35128  bnj999  35140  bnj1398  35216  wevgblacfn  35337  elpotr  36007  dfon2lem8  36016  txpss3v  36104  meran1  36639  arg-ax  36644  bj-sbcex  36991  bj-nfalt  37056  bj-imdirco  37550  difunieq  37736  pibt1  37778  wl-cbvmotv  37884  poimirlem25  38012  poimirlem30  38017  bndss  38153  fldcrngo  38371  flddmn  38425  xrnss3v  38748  trressn  38902  redundss3  39079  redundpim3  39081  eldisjim  39254  eldisjim2  39255  eldisjn0el  39276  partim  39278  mainer  39315  prter1  39371  sn-sup2  42981  fimgmcyclem  43019  mzpclall  43176  setindtrs  43470  dgraalem  43590  oneptri  43702  ifpimim  43953  inintabss  44022  refimssco  44051  cotrintab  44058  intimass  44098  psshepw  44232  nzin  44762  axc11next  44850  iotaexeu  44862  hbexgVD  45349  orbitclmpt  45402  wfaxrep  45438  wfaxsep  45439  wfaxpow  45441  wfaxpr  45442  wfac8prim  45446  permaxinf2lem  45456  absnsb  47490  aovpcov0  47653  aov0ov0  47656  muldvdsfacgt  47849  ichan  47930  ichal  47941  spr0el  47957  sprsymrelf  47970  enege  48136  onego  48137  gbogbow  48247  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgprismgr4cycllem10  48595  sgrpplusgaopALT  48686  rhmsubcALTVlem3  48774  eluz2cnn0n1  49002  regt1loggt0  49027  rege1logbrege0  49049  rege1logbzge0  49050  relogbmulbexp  49052  islan2  50116