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:  norassOLD  1536  hbxfrbi  1828  nexmo  2541  moimi  2545  eu6im  2575  ralimi2  3083  rexbiOLD  3170  reximi2  3171  elex  3440  rmoan  3669  rmoimi2  3673  reuan  3825  sseq2  3943  rabss2  4007  n0rex  4285  undif4  4397  r19.2zb  4423  rzal  4436  difprsnss  4729  snsspw  4772  uniin  4862  iuniin  4933  iuneq1  4937  iuneq2  4940  iunpwss  5032  axrep6  5212  eunex  5308  rmorabex  5369  exss  5372  pwunssOLD  5475  soeq2  5516  elopaelxp  5667  reliin  5716  coeq1  5755  coeq2  5756  cnveq  5771  dmeq  5801  dmin  5809  dmcoss  5869  rncoeq  5873  dminss  6045  imainss  6046  dfco2a  6139  iotaex  6398  fundif  6467  fununi  6493  fof  6672  f1ocnv  6712  foco2  6965  isocnv  7181  isotr  7187  oprabidw  7286  oprabid  7287  zfrep6  7771  ovmptss  7904  dmtpos  8025  tposfn  8042  smores  8154  omopthlem1  8449  eqer  8491  fsetsspwxp  8599  ixpeq2  8657  enssdom  8720  fiprc  8789  sbthlem9  8831  infensuc  8891  fipwuni  9115  dfom3  9335  r1elss  9495  scott0  9575  fin56  10080  dominf  10132  ac6n  10172  brdom4  10217  dominfac  10260  inawina  10377  eltsk2g  10438  ltsosr  10781  ssxr  10975  recgt0ii  11811  sup2  11861  dfnn2  11916  peano2uz2  12338  eluzp1p1  12539  peano2uz  12570  ubmelfzo  13380  elfzlmr  13429  expclzlem  13734  wrdeq  14167  wwlktovf  14599  fsum2dlem  15410  fprod2dlem  15618  sin02gt0  15829  divalglem6  16035  qredeu  16291  isfunc  17495  xpcbas  17811  drsdirfi  17938  clatl  18141  tsrss  18222  smndex1mgm  18461  gimcnv  18798  gsum2dlem1  19486  gsum2dlem2  19487  lmimcnv  20244  fldidom  20489  xrge0subm  20551  fctop  22062  cctop  22064  alexsubALTlem4  23109  lpbl  23565  xrge0gsumle  23902  xrge0tsms  23903  iirev  23998  iihalf1  24000  iihalf2  24002  iimulcl  24006  vitalilem1  24677  ply1idom  25194  aacjcl  25392  aannenlem2  25394  ang180lem4  25867  lgslem3  26352  tgjustf  26738  axlowdim  27232  axcontlem2  27236  usgrexmplef  27529  cusgrop  27708  rusgrpropedg  27854  spthispth  27995  cycliscrct  28068  wwlksn0  28129  clwwlkccat  28255  clwwlkn  28291  clwwlknonccat  28361  numclwwlk1  28626  nmobndseqi  29042  axhcompl-zf  29261  hhcmpl  29463  shunssi  29631  spansni  29820  pjoml3i  29849  cmcmlem  29854  nonbooli  29914  lnopco0i  30267  pjnmopi  30411  pjnormssi  30431  hatomistici  30625  cvexchi  30632  cmdmdi  30680  mddmdin0i  30694  cdj3lem3b  30703  rmoun  30743  disjin  30826  disjin2  30827  xrge0tsmsd  31219  issgon  31991  sxbrsigalem0  32138  eulerpartlemgs2  32247  ballotlem2  32355  ballotth  32404  bnj945  32653  bnj556  32780  bnj557  32781  bnj607  32796  bnj864  32802  bnj969  32826  bnj999  32838  bnj1398  32914  elpotr  33663  dfon2lem8  33672  ttrcltr  33702  sltval2  33786  madef  33967  lrrecfr  34027  txpss3v  34107  meran1  34527  arg-ax  34532  bj-nfalt  34820  bj-imdirco  35288  difunieq  35472  pibt1  35514  wl-cbvmotv  35599  poimirlem25  35729  poimirlem30  35734  bndss  35871  fldcrng  36089  flddmn  36143  xrnss3v  36429  redundss3  36668  redundpim3  36670  prter1  36820  sn-sup2  40360  mzpclall  40465  setindtrs  40763  dgraalem  40886  ifpimim  41014  inintabss  41075  refimssco  41104  cotrintab  41111  intimass  41151  psshepw  41285  nzin  41825  axc11next  41913  iotaexeu  41925  hbexgVD  42415  absnsb  44408  aovpcov0  44569  aov0ov0  44572  ichan  44795  ichal  44806  spr0el  44822  sprsymrelf  44835  enege  44985  onego  44986  gbogbow  45096  mhmismgmhm  45248  sgrpplusgaopALT  45277  rhmisrnghm  45366  srhmsubclem1  45519  rhmsubcALTVlem3  45552  eluz2cnn0n1  45740  regt1loggt0  45770  rege1logbrege0  45792  rege1logbzge0  45793  relogbmulbexp  45795