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  37395  difunieq  37579  pibt1  37621  wl-cbvmotv  37718  poimirlem25  37846  poimirlem30  37851  bndss  37987  fldcrngo  38205  flddmn  38259  xrnss3v  38576  trressn  38718  redundss3  38895  redundpim3  38897  eldisjim  39053  eldisjim2  39054  eldisjn0el  39075  partim  39077  mainer  39103  prter1  39149  sn-sup2  42756  rimcnv  42782  fimgmcyclem  42798  mzpclall  42979  setindtrs  43277  dgraalem  43397  oneptri  43509  ifpimim  43760  inintabss  43829  refimssco  43858  cotrintab  43865  intimass  43905  psshepw  44039  nzin  44569  axc11next  44657  iotaexeu  44669  hbexgVD  45156  orbitclmpt  45209  wfaxrep  45245  wfaxsep  45246  wfaxpow  45248  wfaxpr  45249  wfac8prim  45253  permaxinf2lem  45263  absnsb  47283  aovpcov0  47446  aov0ov0  47449  ichan  47711  ichal  47722  spr0el  47738  sprsymrelf  47751  enege  47901  onego  47902  gbogbow  48012  gpgvtxedg0  48319  gpgvtxedg1  48320  gpgprismgr4cycllem10  48360  sgrpplusgaopALT  48451  rhmsubcALTVlem3  48539  eluz2cnn0n1  48767  regt1loggt0  48792  rege1logbrege0  48814  rege1logbzge0  48815  relogbmulbexp  48817  islan2  49881