Theorem 3imtr4i 292

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  hbxfrbi  1825  excomimw  2044  nexmo  2534  moimi  2538  eu6im  2568  ralimi2  3061  reximi2  3062  rabid2im  3435  elexOLD  3466  rmoan  3707  rmoimi2  3711  reuan  3856  sstr2  3950  rabss2  4037  n0rex  4316  undif4  4426  r19.2zb  4455  rzal  4468  difprsnss  4759  snsspw  4804  uniin  4891  iuniin  4964  iuneq1  4968  iuneq2  4971  iunpwss  5066  axrep6  5238  axrep6OLD  5239  eunex  5340  rmorabex  5415  exss  5418  soeq2  5561  reliin  5771  coeq1  5811  coeq2  5812  cnveq  5827  dmeq  5857  dmin  5865  dmcoss  5927  rncoeq  5932  dminss  6114  imainss  6115  dfco2a  6207  iotaexOLD  6479  fundif  6549  fununi  6575  fof  6754  f1ocnv  6794  foco2  7063  isocnv  7287  isotr  7293  oprabidw  7400  oprabid  7401  zfrep6  7913  ovmptss  8049  dmtpos  8194  tposfn  8211  smores  8298  omopthlem1  8600  brinxper  8677  eqer  8684  fsetsspwxp  8803  ixpeq2  8861  enssdom  8925  fiprc  8993  sbthlem9  9036  infensuc  9096  fipwuni  9353  dfom3  9576  ttrcltr  9645  r1elss  9735  scott0  9815  fin56  10322  dominf  10374  ac6n  10414  brdom4  10459  dominfac  10502  inawina  10619  eltsk2g  10680  ltsosr  11023  ssxr  11219  recgt0ii  12065  sup2  12115  dfnn2  12175  peano2uz2  12598  eluzp1p1  12797  peano2uz  12836  ubmelfzo  13667  elfzlmr  13718  expclzlem  14024  wrdeq  14477  wwlktovf  14898  fsum2dlem  15712  fprod2dlem  15922  sin02gt0  16136  divalglem6  16344  qredeu  16604  isfunc  17802  xpcbas  18115  drsdirfi  18242  clatl  18443  tsrss  18524  mhmismgmhm  18694  smndex1mgm  18810  gimcnv  19175  gsum2dlem1  19876  gsum2dlem2  19877  rhmisrnghm  20365  subrngrng  20435  srhmsubclem1  20562  fldidom  20656  lmimcnv  20950  xrge0subm  21300  fctop  22867  cctop  22869  alexsubALTlem4  23913  lpbl  24367  xrge0gsumle  24698  xrge0tsms  24699  iirev  24799  iihalf1  24801  iihalf2  24804  iimulcl  24809  vitalilem1  25485  ply1idom  26006  aacjcl  26211  aannenlem2  26213  ang180lem4  26698  lgslem3  27186  sltval2  27544  madef  27740  lrrecfr  27826  norecdiv  28069  elons2  28135  dfn0s2  28200  nnaddscl  28214  nnmulscl  28215  znegscl  28256  uzsind  28269  zs12negscl  28316  renegscl  28325  readdscl  28326  remulscl  28329  tgjustf  28376  axlowdim  28864  axcontlem2  28868  usgrexmplef  29162  cusgrop  29341  rusgrpropedg  29488  spthispth  29627  pthdifv  29633  cycliscrct  29702  wwlksn0  29766  clwwlkccat  29892  clwwlkn  29928  clwwlknonccat  29998  numclwwlk1  30263  nmobndseqi  30681  axhcompl-zf  30900  hhcmpl  31102  shunssi  31270  spansni  31459  pjoml3i  31488  cmcmlem  31493  nonbooli  31553  lnopco0i  31906  pjnmopi  32050  pjnormssi  32070  hatomistici  32264  cvexchi  32271  cmdmdi  32319  mddmdin0i  32333  cdj3lem3b  32342  rmoun  32396  disjin  32488  disjin2  32489  xrge0tsmsd  32975  issgon  34086  sxbrsigalem0  34235  eulerpartlemgs2  34344  ballotlem2  34453  ballotth  34502  bnj945  34736  bnj556  34863  bnj557  34864  bnj607  34879  bnj864  34885  bnj969  34909  bnj999  34921  bnj1398  34997  wevgblacfn  35069  elpotr  35742  dfon2lem8  35751  txpss3v  35839  meran1  36372  arg-ax  36377  bj-nfalt  36672  bj-imdirco  37151  difunieq  37335  pibt1  37377  wl-cbvmotv  37474  poimirlem25  37612  poimirlem30  37617  bndss  37753  fldcrngo  37971  flddmn  38025  xrnss3v  38327  trressn  38409  redundss3  38592  redundpim3  38594  eldisjim  38749  eldisjim2  38750  eldisjn0el  38771  partim  38773  mainer  38799  prter1  38845  sn-sup2  42452  rimcnv  42478  fimgmcyclem  42494  mzpclall  42688  setindtrs  42987  dgraalem  43107  oneptri  43219  ifpimim  43471  inintabss  43540  refimssco  43569  cotrintab  43576  intimass  43616  psshepw  43750  nzin  44280  axc11next  44368  iotaexeu  44380  hbexgVD  44868  orbitclmpt  44921  wfaxrep  44957  wfaxsep  44958  wfaxpow  44960  wfaxpr  44961  wfac8prim  44965  permaxinf2lem  44975  absnsb  47001  aovpcov0  47164  aov0ov0  47167  ichan  47429  ichal  47440  spr0el  47456  sprsymrelf  47469  enege  47619  onego  47620  gbogbow  47730  gpgvtxedg0  48027  gpgvtxedg1  48028  gpgprismgr4cycllem10  48067  sgrpplusgaopALT  48156  rhmsubcALTVlem3  48244  eluz2cnn0n1  48473  regt1loggt0  48498  rege1logbrege0  48520  rege1logbzge0  48521  relogbmulbexp  48523  islan2  49588