Theorem 3imtr4i 295

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  hbxfrbi  1858  excomimw  2079  nexmo  2569  eu6im  2603  ralimi2  3098  reximi2  3099  rabid2im  3447  rmoan  3700  rmoimi2  3704  reuan  3848  sstr2  3920  rabss2OLD  4006  n0rex  4308  undif4  4423  rzal  4453  difprsnss  4764  snsspw  4804  uniinOLD  4897  iuniin  4969  iuneq1  4973  iuneq2  4976  iunpwss  5072  axrep6  5246  eunex  5359  rmorabex  5435  exss  5438  soeq2  5588  reliin  5804  coeq1  5846  coeq2  5847  cnveq  5863  dmeq  5897  dmin  5905  dmcoss  5969  dmcossOLD  5970  rncoeq  5977  dminss  6161  imainss  6162  dfco2a  6266  idresdmsscocnv1  6281  fundifOLD  6619  fununi  6645  fof  6826  f1ocnv  6867  foco2  7141  isocnv  7369  isotr  7375  oprabidw  7482  oprabid  7483  zfrep6OLD  8001  ovmptssOLD  8140  dmtpos  8293  tposfn  8310  smores  8398  omopthlem1  8706  brinxper  8785  eqer  8792  fsetsspwxp  8913  ixpeq2  8977  enssdomOLD  9042  fiprc  9110  sbthlem9  9152  infensuc  9212  fipwuni  9455  dfom3  9685  ttrcltr  9754  r1elss  9851  scott0b  9974  scott0OLD  9975  fin56  10510  dominf  10562  ac6n  10602  brdom4  10648  dominfac  10697  inawina  10814  eltsk2g  10875  ltsosr  11218  ssxr  11418  recgt0ii  12263  sup2  12313  dfnn2  12388  peano2uz2  12827  eluzp1p1  13033  peano2uz  13068  ubmelfzo  13905  elfzlmr  13957  expclzlem  14266  wrdeq  14722  wwlktovf  15152  fsum2dlem  15980  fprod2dlem  16191  sin02gt0  16404  divalglem6  16612  qredeu  16877  isfunc  18089  xpcbas  18402  drsdirfi  18529  clatl  18732  tsrss  18813  mhmismgmhm  19036  smndex1mgm  19156  gimcnv  19531  gsum2dlem1  20235  gsum2dlem2  20236  rhmisrnghm  20762  rimcnv  20768  subrngrng  20853  srhmsubclem1  20980  fldidom  21080  lmimcnv  21393  xrge0subm  21803  fctop  23377  cctop  23379  alexsubALTlem4  24424  lpbl  24877  xrge0gsumle  25208  xrge0tsms  25209  iirev  25305  iihalf1  25307  iihalf2  25309  iimulcl  25313  vitalilem1  25984  ply1idom  26498  aacjcl  26711  aannenlem2  26713  ang180lem4  27197  lgslem3  27683  ltsval2  28070  madef  28279  lrrecfr  28386  norecdiv  28633  elons2  28701  dfn0s2  28775  nnaddscl  28789  nnmulscl  28790  znegscl  28835  uzsind  28848  zsoring  28852  z12negscl  28921  renegscl  28941  readdscl  28942  remulscl  28945  tgjustf  28992  axlowdim  29596  axcontlem2  29600  usgrexmplef  29897  cusgrop  30076  rusgrpropedg  30222  spthispth  30366  pthdifv  30373  cycliscrct  30444  wwlksn0  30509  clwwlkccat  30638  clwwlkn  30674  clwwlknonccat  30744  numclwwlk1  31019  nmobndseqi  31438  axhcompl-zf  31657  hhcmpl  31859  shunssi  32027  spansni  32216  pjoml3i  32245  cmcmlem  32250  nonbooli  32310  lnopco0i  32663  pjnmopi  32807  pjnormssi  32827  hatomistici  33021  cvexchi  33028  cmdmdi  33076  mddmdin0i  33090  cdj3lem3b  33099  rmoun  33189  disjin  33278  disjin2  33279  xrge0tsmsd  33733  issgon  34866  sxbrsigalem0  35014  eulerpartlemgs2  35123  ballotlem2  35232  ballotth  35281  bnj945  35515  bnj556  35641  bnj557  35642  bnj607  35657  bnj864  35663  bnj969  35687  bnj999  35699  bnj1398  35775  rankse  35864  kardexen  35972  wevgblacfn  36080  vsmrep  36131  elpotr  36758  dfon2lem8  36767  txpss3v  36855  meran1  37414  arg-ax  37419  bj-sbcex  37765  bj-nfalt  37830  bj-imdirco  38379  difunieq  38565  pibt1  38607  wl-cbvmotv  38713  poimirlem25  38831  poimirlem30  38836  bndss  38986  fldcrngo  39204  flddmn  39258  xrnss3v  39579  trressn  39733  redundss3  39910  redundpim3  39912  eldisjim  40085  eldisjim2  40086  eldisjn0el  40107  partim  40109  mainer  40146  prter1  40202  sn-sup2  43821  fimgmcyclem  43863  mzpclall  44004  setindtrs  44298  dgraalem  44412  oneptri  44520  ifpimim  44771  inintabss  44840  refimssco  44868  cotrintab  44875  intimass  44915  psshepw  45049  nzin  45563  axc11next  45651  iotaexeu  45662  hbexgVD  46148  orbitclmpt  46212  wfaxrep  46248  wfaxsep  46249  wfaxpow  46251  wfaxpr  46252  wfac8prim  46256  permaxinf2lem  46266  absnsb  48370  aovpcov0  48533  aov0ov0  48536  muldvdsfacgt  48729  ichan  48810  ichal  48821  spr0el  48837  sprsymrelf  48850  enege  49016  onego  49017  gbogbow  49127  gpgvtxedg0  49434  gpgvtxedg1  49435  gpgprismgr4cycllem10  49475  sgrpplusgaopALT  49565  rhmsubcALTVlem3  49653  eluz2cnn0n1  49954  regt1loggt0  49979  rege1logbrege0  50001  rege1logbzge0  50002  relogbmulbexp  50004  islan2  51140  alseuals  51348  ralseurals  51349