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  1823  excomimw  2043  nexmo  2544  moimi  2548  eu6im  2578  ralimi2  3084  reximi2  3085  rexbiOLD  3111  rabid2im  3477  elexOLD  3510  rmoan  3761  rmoimi2  3765  reuan  3918  sstr2  4015  sseq2  4035  rabss2  4101  n0rex  4380  undif4  4490  r19.2zb  4519  rzal  4532  difprsnss  4824  snsspw  4869  uniin  4955  iuniin  5027  iuneq1  5031  iuneq2  5034  iunpwss  5130  axrep6  5310  eunex  5408  rmorabex  5480  exss  5483  soeq2  5630  elopaelxpOLD  5790  reliin  5841  coeq1  5882  coeq2  5883  cnveq  5898  dmeq  5928  dmin  5936  dmcoss  5997  rncoeq  6002  dminss  6184  imainss  6185  dfco2a  6277  iotaexOLD  6553  fundif  6627  fununi  6653  fof  6834  f1ocnv  6874  foco2  7143  isocnv  7366  isotr  7372  oprabidw  7479  oprabid  7480  zfrep6  7995  ovmptss  8134  dmtpos  8279  tposfn  8296  smores  8408  omopthlem1  8715  brinxper  8792  eqer  8799  fsetsspwxp  8911  ixpeq2  8969  enssdom  9037  fiprc  9111  sbthlem9  9157  infensuc  9221  fipwuni  9495  dfom3  9716  ttrcltr  9785  r1elss  9875  scott0  9955  fin56  10462  dominf  10514  ac6n  10554  brdom4  10599  dominfac  10642  inawina  10759  eltsk2g  10820  ltsosr  11163  ssxr  11359  recgt0ii  12201  sup2  12251  dfnn2  12306  peano2uz2  12731  eluzp1p1  12931  peano2uz  12966  ubmelfzo  13781  elfzlmr  13831  expclzlem  14134  wrdeq  14584  wwlktovf  15005  fsum2dlem  15818  fprod2dlem  16028  sin02gt0  16240  divalglem6  16446  qredeu  16705  isfunc  17928  xpcbas  18247  drsdirfi  18375  clatl  18578  tsrss  18659  mhmismgmhm  18826  smndex1mgm  18942  gimcnv  19307  gsum2dlem1  20012  gsum2dlem2  20013  rhmisrnghm  20506  subrngrng  20576  srhmsubclem1  20699  fldidom  20793  lmimcnv  21089  xrge0subm  21448  fctop  23032  cctop  23034  alexsubALTlem4  24079  lpbl  24537  xrge0gsumle  24874  xrge0tsms  24875  iirev  24975  iihalf1  24977  iihalf2  24980  iimulcl  24985  vitalilem1  25662  ply1idom  26184  aacjcl  26387  aannenlem2  26389  ang180lem4  26873  lgslem3  27361  sltval2  27719  madef  27913  lrrecfr  27994  norecdiv  28234  elons2  28299  dfn0s2  28354  nnaddscl  28367  nnmulscl  28368  znegscl  28396  uzsind  28409  renegscl  28448  readdscl  28449  remulscl  28452  tgjustf  28499  axlowdim  28994  axcontlem2  28998  usgrexmplef  29294  cusgrop  29473  rusgrpropedg  29620  spthispth  29762  cycliscrct  29835  wwlksn0  29896  clwwlkccat  30022  clwwlkn  30058  clwwlknonccat  30128  numclwwlk1  30393  nmobndseqi  30811  axhcompl-zf  31030  hhcmpl  31232  shunssi  31400  spansni  31589  pjoml3i  31618  cmcmlem  31623  nonbooli  31683  lnopco0i  32036  pjnmopi  32180  pjnormssi  32200  hatomistici  32394  cvexchi  32401  cmdmdi  32449  mddmdin0i  32463  cdj3lem3b  32472  rmoun  32522  disjin  32608  disjin2  32609  xrge0tsmsd  33041  issgon  34087  sxbrsigalem0  34236  eulerpartlemgs2  34345  ballotlem2  34453  ballotth  34502  bnj945  34749  bnj556  34876  bnj557  34877  bnj607  34892  bnj864  34898  bnj969  34922  bnj999  34934  bnj1398  35010  wevgblacfn  35076  elpotr  35745  dfon2lem8  35754  txpss3v  35842  meran1  36377  arg-ax  36382  bj-nfalt  36677  bj-imdirco  37156  difunieq  37340  pibt1  37382  wl-cbvmotv  37467  poimirlem25  37605  poimirlem30  37610  bndss  37746  fldcrngo  37964  flddmn  38018  xrnss3v  38328  trressn  38401  redundss3  38584  redundpim3  38586  eldisjim  38740  eldisjim2  38741  eldisjn0el  38762  partim  38764  mainer  38790  prter1  38835  sn-sup2  42447  rimcnv  42472  fimgmcyclem  42488  mzpclall  42683  setindtrs  42982  dgraalem  43102  oneptri  43218  ifpimim  43471  inintabss  43540  refimssco  43569  cotrintab  43576  intimass  43616  psshepw  43750  nzin  44287  axc11next  44375  iotaexeu  44387  hbexgVD  44877  absnsb  46942  aovpcov0  47105  aov0ov0  47108  ichan  47329  ichal  47340  spr0el  47356  sprsymrelf  47369  enege  47519  onego  47520  gbogbow  47630  sgrpplusgaopALT  47918  rhmsubcALTVlem3  48006  eluz2cnn0n1  48240  regt1loggt0  48270  rege1logbrege0  48292  rege1logbzge0  48293  relogbmulbexp  48295