Theorem 3imtr4i 294

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  hbxfrbi  1845  excomimw  2064  nexmo  2568  eu6im  2602  ralimi2  3094  reximi2  3095  rabid2im  3446  rmoan  3702  rmoimi2  3706  reuan  3849  sstr2  3943  rabss2OLD  4031  n0rex  4310  undif4  4421  rzal  4448  difprsnss  4759  snsspw  4802  uniinOLD  4890  iuniin  4962  iuneq1  4966  iuneq2  4969  iunpwss  5064  axrep6  5236  axrep6OLD  5237  eunex  5347  rmorabex  5427  exss  5430  soeq2  5577  reliin  5790  coeq1  5829  coeq2  5830  cnveq  5845  dmeq  5879  dmin  5887  dmcoss  5951  dmcossOLD  5952  rncoeq  5958  dminss  6138  imainss  6139  dfco2a  6233  fundif  6570  fununi  6596  fof  6778  f1ocnv  6819  foco2  7090  isocnv  7314  isotr  7320  oprabidw  7427  oprabid  7428  zfrep6OLD  7936  ovmptss  8072  dmtpos  8218  tposfn  8235  smores  8323  omopthlem1  8629  brinxper  8708  eqer  8715  fsetsspwxp  8834  ixpeq2  8893  enssdomOLD  8958  fiprc  9025  sbthlem9  9067  infensuc  9127  fipwuni  9372  dfom3  9602  ttrcltr  9671  r1elss  9764  scott0  9844  fin56  10350  dominf  10402  ac6n  10442  brdom4  10487  dominfac  10531  inawina  10648  eltsk2g  10709  ltsosr  11052  ssxr  11252  recgt0ii  12098  sup2  12148  dfnn2  12223  peano2uz2  12661  eluzp1p1  12867  peano2uz  12902  ubmelfzo  13736  elfzlmr  13788  expclzlem  14096  wrdeq  14549  wwlktovf  14969  fsum2dlem  15797  fprod2dlem  16010  sin02gt0  16224  divalglem6  16432  qredeu  16692  isfunc  17897  xpcbas  18210  drsdirfi  18337  clatl  18540  tsrss  18621  mhmismgmhm  18825  smndex1mgm  18944  gimcnv  19307  gsum2dlem1  20010  gsum2dlem2  20011  rhmisrnghm  20529  rimcnv  20534  subrngrng  20600  srhmsubclem1  20727  fldidom  20821  lmimcnv  21134  xrge0subm  21495  fctop  23064  cctop  23066  alexsubALTlem4  24110  lpbl  24563  xrge0gsumle  24894  xrge0tsms  24895  iirev  24991  iihalf1  24993  iihalf2  24995  iimulcl  24999  vitalilem1  25670  ply1idom  26185  aacjcl  26391  aannenlem2  26393  ang180lem4  26877  lgslem3  27363  ltsval2  27720  madef  27929  lrrecfr  28036  norecdiv  28283  elons2  28351  dfn0s2  28425  nnaddscl  28439  nnmulscl  28440  znegscl  28485  uzsind  28498  zsoring  28502  z12negscl  28571  renegscl  28591  readdscl  28592  remulscl  28595  tgjustf  28642  axlowdim  29162  axcontlem2  29166  usgrexmplef  29460  cusgrop  29639  rusgrpropedg  29785  spthispth  29924  pthdifv  29930  cycliscrct  29999  wwlksn0  30063  clwwlkccat  30192  clwwlkn  30228  clwwlknonccat  30298  numclwwlk1  30563  nmobndseqi  30982  axhcompl-zf  31201  hhcmpl  31403  shunssi  31571  spansni  31760  pjoml3i  31789  cmcmlem  31794  nonbooli  31854  lnopco0i  32207  pjnmopi  32351  pjnormssi  32371  hatomistici  32565  cvexchi  32572  cmdmdi  32620  mddmdin0i  32634  cdj3lem3b  32643  rmoun  32693  disjin  32786  disjin2  32787  xrge0tsmsd  33253  issgon  34420  sxbrsigalem0  34568  eulerpartlemgs2  34677  ballotlem2  34786  ballotth  34835  bnj945  35069  bnj556  35195  bnj557  35196  bnj607  35211  bnj864  35217  bnj969  35241  bnj999  35253  bnj1398  35329  wevgblacfn  35454  elpotr  36129  dfon2lem8  36138  txpss3v  36226  meran1  36771  arg-ax  36776  bj-sbcex  37123  bj-nfalt  37188  bj-imdirco  37682  difunieq  37868  pibt1  37910  wl-cbvmotv  38016  poimirlem25  38144  poimirlem30  38149  bndss  38285  fldcrngo  38503  flddmn  38557  xrnss3v  38880  trressn  39034  redundss3  39211  redundpim3  39213  eldisjim  39386  eldisjim2  39387  eldisjn0el  39408  partim  39410  mainer  39447  prter1  39503  sn-sup2  43113  fimgmcyclem  43151  mzpclall  43308  setindtrs  43602  dgraalem  43722  oneptri  43834  ifpimim  44085  inintabss  44154  refimssco  44183  cotrintab  44190  intimass  44230  psshepw  44364  nzin  44894  axc11next  44982  iotaexeu  44994  hbexgVD  45481  orbitclmpt  45534  wfaxrep  45570  wfaxsep  45571  wfaxpow  45573  wfaxpr  45574  wfac8prim  45578  permaxinf2lem  45588  absnsb  47621  aovpcov0  47784  aov0ov0  47787  muldvdsfacgt  47980  ichan  48061  ichal  48072  spr0el  48088  sprsymrelf  48101  enege  48267  onego  48268  gbogbow  48378  gpgvtxedg0  48685  gpgvtxedg1  48686  gpgprismgr4cycllem10  48726  sgrpplusgaopALT  48817  rhmsubcALTVlem3  48905  eluz2cnn0n1  49133  regt1loggt0  49158  rege1logbrege0  49180  rege1logbzge0  49181  relogbmulbexp  49183  islan2  50247