Theorem 3imtr4i 291

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  hbxfrbi  1827  nexmo  2535  moimi  2539  eu6im  2569  ralimi2  3078  reximi2  3079  rexbiOLD  3105  elex  3492  rmoan  3735  rmoimi2  3739  reuan  3890  sseq2  4008  rabss2  4075  n0rex  4354  undif4  4466  r19.2zb  4495  rzal  4508  difprsnss  4802  snsspw  4845  uniin  4935  iuniin  5009  iuneq1  5013  iuneq2  5016  iunpwss  5110  axrep6  5292  eunex  5388  rmorabex  5460  exss  5463  soeq2  5610  elopaelxpOLD  5766  reliin  5817  coeq1  5857  coeq2  5858  cnveq  5873  dmeq  5903  dmin  5911  dmcoss  5970  rncoeq  5974  dminss  6152  imainss  6153  dfco2a  6245  iotaexOLD  6523  fundif  6597  fununi  6623  fof  6805  f1ocnv  6845  foco2  7110  isocnv  7329  isotr  7335  oprabidw  7442  oprabid  7443  zfrep6  7943  ovmptss  8081  dmtpos  8225  tposfn  8242  smores  8354  omopthlem1  8660  eqer  8740  fsetsspwxp  8849  ixpeq2  8907  enssdom  8975  fiprc  9047  sbthlem9  9093  infensuc  9157  fipwuni  9423  dfom3  9644  ttrcltr  9713  r1elss  9803  scott0  9883  fin56  10390  dominf  10442  ac6n  10482  brdom4  10527  dominfac  10570  inawina  10687  eltsk2g  10748  ltsosr  11091  ssxr  11287  recgt0ii  12124  sup2  12174  dfnn2  12229  peano2uz2  12654  eluzp1p1  12854  peano2uz  12889  ubmelfzo  13701  elfzlmr  13750  expclzlem  14053  wrdeq  14490  wwlktovf  14911  fsum2dlem  15720  fprod2dlem  15928  sin02gt0  16139  divalglem6  16345  qredeu  16599  isfunc  17818  xpcbas  18134  drsdirfi  18262  clatl  18465  tsrss  18546  mhmismgmhm  18713  smndex1mgm  18824  gimcnv  19181  gsum2dlem1  19879  gsum2dlem2  19880  rhmisrnghm  20371  subrngrng  20438  lmimcnv  20822  fldidom  21123  xrge0subm  21186  fctop  22727  cctop  22729  alexsubALTlem4  23774  lpbl  24232  xrge0gsumle  24569  xrge0tsms  24570  iirev  24669  iihalf1  24671  iihalf2  24673  iimulcl  24677  vitalilem1  25349  ply1idom  25866  aacjcl  26064  aannenlem2  26066  ang180lem4  26541  lgslem3  27026  sltval2  27383  madef  27576  lrrecfr  27653  norecdiv  27865  elons2  27912  dfn0s2  27929  n0sind  27930  tgjustf  27979  axlowdim  28474  axcontlem2  28478  usgrexmplef  28771  cusgrop  28950  rusgrpropedg  29096  spthispth  29238  cycliscrct  29311  wwlksn0  29372  clwwlkccat  29498  clwwlkn  29534  clwwlknonccat  29604  numclwwlk1  29869  nmobndseqi  30287  axhcompl-zf  30506  hhcmpl  30708  shunssi  30876  spansni  31065  pjoml3i  31094  cmcmlem  31099  nonbooli  31159  lnopco0i  31512  pjnmopi  31656  pjnormssi  31676  hatomistici  31870  cvexchi  31877  cmdmdi  31925  mddmdin0i  31939  cdj3lem3b  31948  rmoun  31989  disjin  32072  disjin2  32073  xrge0tsmsd  32467  issgon  33407  sxbrsigalem0  33556  eulerpartlemgs2  33665  ballotlem2  33773  ballotth  33822  bnj945  34070  bnj556  34197  bnj557  34198  bnj607  34213  bnj864  34219  bnj969  34243  bnj999  34255  bnj1398  34331  elpotr  35045  dfon2lem8  35054  txpss3v  35142  meran1  35599  arg-ax  35604  bj-nfalt  35892  bj-imdirco  36374  difunieq  36558  pibt1  36600  wl-cbvmotv  36685  poimirlem25  36816  poimirlem30  36821  bndss  36957  fldcrngo  37175  flddmn  37229  xrnss3v  37545  trressn  37618  redundss3  37801  redundpim3  37803  eldisjim  37957  eldisjim2  37958  eldisjn0el  37979  partim  37981  mainer  38007  prter1  38052  rimcnv  41396  sn-sup2  41644  mzpclall  41767  setindtrs  42066  dgraalem  42189  oneptri  42308  ifpimim  42562  inintabss  42631  refimssco  42660  cotrintab  42667  intimass  42707  psshepw  42841  nzin  43379  axc11next  43467  iotaexeu  43479  hbexgVD  43969  absnsb  46036  aovpcov0  46197  aov0ov0  46200  ichan  46422  ichal  46433  spr0el  46449  sprsymrelf  46462  enege  46612  onego  46613  gbogbow  46723  sgrpplusgaopALT  46872  srhmsubclem1  47060  rhmsubcALTVlem3  47093  eluz2cnn0n1  47280  regt1loggt0  47310  rege1logbrege0  47332  rege1logbzge0  47333  relogbmulbexp  47335