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  2077  nexmo  2566  eu6im  2600  ralimi2  3094  reximi2  3095  rabid2im  3443  rmoan  3697  rmoimi2  3701  reuan  3844  sstr2  3938  rabss2OLD  4026  n0rex  4305  undif4  4420  rzal  4450  difprsnss  4762  snsspw  4804  uniinOLD  4892  iuniin  4964  iuneq1  4968  iuneq2  4971  iunpwss  5067  axrep6  5241  axrep6OLD  5242  eunex  5355  rmorabex  5435  exss  5438  soeq2  5585  reliin  5798  coeq1  5837  coeq2  5838  cnveq  5853  dmeq  5887  dmin  5895  dmcoss  5959  dmcossOLD  5960  rncoeq  5965  dminss  6144  imainss  6145  dfco2a  6242  fundif  6583  fununi  6609  fof  6790  f1ocnv  6831  foco2  7103  isocnv  7332  isotr  7338  oprabidw  7445  oprabid  7446  zfrep6OLD  7953  ovmptss  8091  dmtpos  8237  tposfn  8254  smores  8342  omopthlem1  8650  brinxper  8729  eqer  8736  fsetsspwxp  8857  ixpeq2  8921  enssdomOLD  8986  fiprc  9054  sbthlem9  9096  infensuc  9156  fipwuni  9399  dfom3  9629  ttrcltr  9698  r1elss  9791  scott0b  9879  scott0OLD  9880  fin56  10398  dominf  10450  ac6n  10490  brdom4  10536  dominfac  10585  inawina  10702  eltsk2g  10763  ltsosr  11106  ssxr  11306  recgt0ii  12148  sup2  12198  dfnn2  12273  peano2uz2  12712  eluzp1p1  12918  peano2uz  12953  ubmelfzo  13789  elfzlmr  13841  expclzlem  14150  wrdeq  14604  wwlktovf  15032  fsum2dlem  15859  fprod2dlem  16070  sin02gt0  16283  divalglem6  16491  qredeu  16751  isfunc  17956  xpcbas  18269  drsdirfi  18396  clatl  18599  tsrss  18680  mhmismgmhm  18902  smndex1mgm  19022  gimcnv  19397  gsum2dlem1  20100  gsum2dlem2  20101  rhmisrnghm  20625  rimcnv  20631  subrngrng  20715  srhmsubclem1  20842  fldidom  20941  lmimcnv  21254  xrge0subm  21659  fctop  23232  cctop  23234  alexsubALTlem4  24279  lpbl  24732  xrge0gsumle  25063  xrge0tsms  25064  iirev  25160  iihalf1  25162  iihalf2  25164  iimulcl  25168  vitalilem1  25839  ply1idom  26353  aacjcl  26566  aannenlem2  26568  ang180lem4  27052  lgslem3  27538  ltsval2  27895  madef  28104  lrrecfr  28211  norecdiv  28458  elons2  28526  dfn0s2  28600  nnaddscl  28614  nnmulscl  28615  znegscl  28660  uzsind  28673  zsoring  28677  z12negscl  28746  renegscl  28766  readdscl  28767  remulscl  28770  tgjustf  28817  axlowdim  29421  axcontlem2  29425  usgrexmplef  29722  cusgrop  29901  rusgrpropedg  30047  spthispth  30191  pthdifv  30198  cycliscrct  30269  wwlksn0  30334  clwwlkccat  30463  clwwlkn  30499  clwwlknonccat  30569  numclwwlk1  30844  nmobndseqi  31263  axhcompl-zf  31482  hhcmpl  31684  shunssi  31852  spansni  32041  pjoml3i  32070  cmcmlem  32075  nonbooli  32135  lnopco0i  32488  pjnmopi  32632  pjnormssi  32652  hatomistici  32846  cvexchi  32853  cmdmdi  32901  mddmdin0i  32915  cdj3lem3b  32924  rmoun  32972  disjin  33062  disjin2  33063  xrge0tsmsd  33516  issgon  34636  sxbrsigalem0  34785  eulerpartlemgs2  34894  ballotlem2  35003  ballotth  35052  bnj945  35286  bnj556  35412  bnj557  35413  bnj607  35428  bnj864  35434  bnj969  35458  bnj999  35470  bnj1398  35546  kardexen  35692  wevgblacfn  35711  elpotr  36361  dfon2lem8  36370  txpss3v  36458  meran1  37033  arg-ax  37038  bj-sbcex  37384  bj-nfalt  37449  bj-imdirco  37945  difunieq  38131  pibt1  38173  wl-cbvmotv  38279  poimirlem25  38397  poimirlem30  38402  bndss  38539  fldcrngo  38757  flddmn  38811  xrnss3v  39132  trressn  39286  redundss3  39463  redundpim3  39465  eldisjim  39638  eldisjim2  39639  eldisjn0el  39660  partim  39662  mainer  39699  prter1  39755  sn-sup2  43382  fimgmcyclem  43418  mzpclall  43575  setindtrs  43869  dgraalem  43989  oneptri  44101  ifpimim  44352  inintabss  44421  refimssco  44450  cotrintab  44457  intimass  44497  psshepw  44631  nzin  45145  axc11next  45233  iotaexeu  45245  hbexgVD  45731  orbitclmpt  45784  wfaxrep  45820  wfaxsep  45821  wfaxpow  45823  wfaxpr  45824  wfac8prim  45828  permaxinf2lem  45838  absnsb  47918  aovpcov0  48081  aov0ov0  48084  muldvdsfacgt  48277  ichan  48358  ichal  48369  spr0el  48385  sprsymrelf  48398  enege  48564  onego  48565  gbogbow  48675  gpgvtxedg0  48982  gpgvtxedg1  48983  gpgprismgr4cycllem10  49023  sgrpplusgaopALT  49113  rhmsubcALTVlem3  49201  eluz2cnn0n1  49444  regt1loggt0  49469  rege1logbrege0  49491  rege1logbzge0  49492  relogbmulbexp  49494  islan2  50555  alseuals  50756  ralseurals  50757