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  1826  excomimw  2045  nexmo  2541  eu6im  2575  ralimi2  3068  reximi2  3069  rabid2im  3431  elexOLD  3462  rmoan  3697  rmoimi2  3701  reuan  3846  sstr2  3940  rabss2OLD  4030  n0rex  4309  undif4  4419  rzal  4447  difprsnss  4755  snsspw  4800  uniin  4887  iuniin  4959  iuneq1  4963  iuneq2  4966  iunpwss  5062  axrep6  5233  axrep6OLD  5234  eunex  5335  rmorabex  5408  exss  5411  soeq2  5554  reliin  5766  coeq1  5806  coeq2  5807  cnveq  5822  dmeq  5852  dmin  5860  dmcoss  5924  dmcossOLD  5925  rncoeq  5931  dminss  6111  imainss  6112  dfco2a  6204  fundif  6541  fununi  6567  fof  6746  f1ocnv  6786  foco2  7054  isocnv  7276  isotr  7282  oprabidw  7389  oprabid  7390  zfrep6  7899  ovmptss  8035  dmtpos  8180  tposfn  8197  smores  8284  omopthlem1  8587  brinxper  8664  eqer  8671  fsetsspwxp  8790  ixpeq2  8849  enssdomOLD  8914  fiprc  8981  sbthlem9  9023  infensuc  9083  fipwuni  9329  dfom3  9556  ttrcltr  9625  r1elss  9718  scott0  9798  fin56  10303  dominf  10355  ac6n  10395  brdom4  10440  dominfac  10484  inawina  10601  eltsk2g  10662  ltsosr  11005  ssxr  11202  recgt0ii  12048  sup2  12098  dfnn2  12158  peano2uz2  12580  eluzp1p1  12779  peano2uz  12814  ubmelfzo  13646  elfzlmr  13698  expclzlem  14006  wrdeq  14459  wwlktovf  14879  fsum2dlem  15693  fprod2dlem  15903  sin02gt0  16117  divalglem6  16325  qredeu  16585  isfunc  17788  xpcbas  18101  drsdirfi  18228  clatl  18431  tsrss  18512  mhmismgmhm  18716  smndex1mgm  18832  gimcnv  19196  gsum2dlem1  19899  gsum2dlem2  19900  rhmisrnghm  20416  subrngrng  20483  srhmsubclem1  20610  fldidom  20704  lmimcnv  21019  xrge0subm  21398  fctop  22948  cctop  22950  alexsubALTlem4  23994  lpbl  24447  xrge0gsumle  24778  xrge0tsms  24779  iirev  24879  iihalf1  24881  iihalf2  24884  iimulcl  24889  vitalilem1  25565  ply1idom  26086  aacjcl  26291  aannenlem2  26293  ang180lem4  26778  lgslem3  27266  ltsval2  27624  madef  27832  lrrecfr  27939  norecdiv  28186  elons2  28254  dfn0s2  28328  nnaddscl  28342  nnmulscl  28343  znegscl  28388  uzsind  28401  zsoring  28405  z12negscl  28474  renegscl  28494  readdscl  28495  remulscl  28498  tgjustf  28545  axlowdim  29034  axcontlem2  29038  usgrexmplef  29332  cusgrop  29511  rusgrpropedg  29658  spthispth  29797  pthdifv  29803  cycliscrct  29872  wwlksn0  29936  clwwlkccat  30065  clwwlkn  30101  clwwlknonccat  30171  numclwwlk1  30436  nmobndseqi  30854  axhcompl-zf  31073  hhcmpl  31275  shunssi  31443  spansni  31632  pjoml3i  31661  cmcmlem  31666  nonbooli  31726  lnopco0i  32079  pjnmopi  32223  pjnormssi  32243  hatomistici  32437  cvexchi  32444  cmdmdi  32492  mddmdin0i  32506  cdj3lem3b  32515  rmoun  32568  disjin  32661  disjin2  32662  xrge0tsmsd  33155  issgon  34280  sxbrsigalem0  34428  eulerpartlemgs2  34537  ballotlem2  34646  ballotth  34695  bnj945  34929  bnj556  35056  bnj557  35057  bnj607  35072  bnj864  35078  bnj969  35102  bnj999  35114  bnj1398  35190  wevgblacfn  35303  elpotr  35973  dfon2lem8  35982  txpss3v  36070  meran1  36605  arg-ax  36610  bj-nfalt  36912  bj-imdirco  37391  difunieq  37575  pibt1  37617  wl-cbvmotv  37714  poimirlem25  37842  poimirlem30  37847  bndss  37983  fldcrngo  38201  flddmn  38255  xrnss3v  38562  trressn  38704  redundss3  38881  redundpim3  38883  eldisjim  39039  eldisjim2  39040  eldisjn0el  39061  partim  39063  mainer  39089  prter1  39135  sn-sup2  42742  rimcnv  42768  fimgmcyclem  42784  mzpclall  42965  setindtrs  43263  dgraalem  43383  oneptri  43495  ifpimim  43746  inintabss  43815  refimssco  43844  cotrintab  43851  intimass  43891  psshepw  44025  nzin  44555  axc11next  44643  iotaexeu  44655  hbexgVD  45142  orbitclmpt  45195  wfaxrep  45231  wfaxsep  45232  wfaxpow  45234  wfaxpr  45235  wfac8prim  45239  permaxinf2lem  45249  absnsb  47269  aovpcov0  47432  aov0ov0  47435  ichan  47697  ichal  47708  spr0el  47724  sprsymrelf  47737  enege  47887  onego  47888  gbogbow  47998  gpgvtxedg0  48305  gpgvtxedg1  48306  gpgprismgr4cycllem10  48346  sgrpplusgaopALT  48437  rhmsubcALTVlem3  48525  eluz2cnn0n1  48753  regt1loggt0  48778  rege1logbrege0  48800  rege1logbzge0  48801  relogbmulbexp  48803  islan2  49867