Theorem 3imtr4i 295

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  hbxfrbi  1858  excomimw  2077  nexmo  2572  eu6im  2606  ralimi2  3100  reximi2  3101  rabid2im  3451  rmoan  3705  rmoimi2  3709  reuan  3853  sstr2  3947  rabss2OLD  4035  n0rex  4315  undif4  4430  rzal  4458  difprsnss  4770  snsspw  4812  uniinOLD  4900  iuniin  4972  iuneq1  4976  iuneq2  4979  iunpwss  5076  axrep6  5250  axrep6OLD  5251  eunex  5364  rmorabex  5444  exss  5447  soeq2  5594  reliin  5807  coeq1  5846  coeq2  5847  cnveq  5862  dmeq  5896  dmin  5904  dmcoss  5968  dmcossOLD  5969  rncoeq  5974  dminss  6153  imainss  6154  dfco2a  6250  fundif  6589  fununi  6615  fof  6796  f1ocnv  6837  foco2  7108  isocnv  7332  isotr  7338  oprabidw  7447  oprabid  7448  zfrep6OLD  7954  ovmptss  8090  dmtpos  8236  tposfn  8253  smores  8341  omopthlem1  8647  brinxper  8726  eqer  8733  fsetsspwxp  8852  ixpeq2  8911  enssdomOLD  8976  fiprc  9043  sbthlem9  9085  infensuc  9145  fipwuni  9388  dfom3  9618  ttrcltr  9687  r1elss  9780  scott0b  9868  scott0OLD  9869  fin56  10387  dominf  10439  ac6n  10479  brdom4  10524  dominfac  10568  inawina  10685  eltsk2g  10746  ltsosr  11089  ssxr  11289  recgt0ii  12131  sup2  12181  dfnn2  12256  peano2uz2  12694  eluzp1p1  12900  peano2uz  12935  ubmelfzo  13770  elfzlmr  13822  expclzlem  14130  wrdeq  14584  wwlktovf  15004  fsum2dlem  15832  fprod2dlem  16045  sin02gt0  16258  divalglem6  16466  qredeu  16726  isfunc  17931  xpcbas  18244  drsdirfi  18371  clatl  18574  tsrss  18655  mhmismgmhm  18859  smndex1mgm  18979  gimcnv  19347  gsum2dlem1  20050  gsum2dlem2  20051  rhmisrnghm  20574  rimcnv  20580  subrngrng  20664  srhmsubclem1  20791  fldidom  20890  lmimcnv  21203  xrge0subm  21608  fctop  23176  cctop  23178  alexsubALTlem4  24222  lpbl  24675  xrge0gsumle  25006  xrge0tsms  25007  iirev  25103  iihalf1  25105  iihalf2  25107  iimulcl  25111  vitalilem1  25782  ply1idom  26297  aacjcl  26505  aannenlem2  26507  ang180lem4  26992  lgslem3  27478  ltsval2  27835  madef  28044  lrrecfr  28151  norecdiv  28398  elons2  28466  dfn0s2  28540  nnaddscl  28554  nnmulscl  28555  znegscl  28600  uzsind  28613  zsoring  28617  z12negscl  28686  renegscl  28706  readdscl  28707  remulscl  28710  tgjustf  28757  axlowdim  29326  axcontlem2  29330  usgrexmplef  29624  cusgrop  29803  rusgrpropedg  29949  spthispth  30088  pthdifv  30094  cycliscrct  30163  wwlksn0  30227  clwwlkccat  30356  clwwlkn  30392  clwwlknonccat  30462  numclwwlk1  30727  nmobndseqi  31146  axhcompl-zf  31365  hhcmpl  31567  shunssi  31735  spansni  31924  pjoml3i  31953  cmcmlem  31958  nonbooli  32018  lnopco0i  32371  pjnmopi  32515  pjnormssi  32535  hatomistici  32729  cvexchi  32736  cmdmdi  32784  mddmdin0i  32798  cdj3lem3b  32807  rmoun  32855  disjin  32946  disjin2  32947  xrge0tsmsd  33406  issgon  34526  sxbrsigalem0  34674  eulerpartlemgs2  34783  ballotlem2  34892  ballotth  34941  bnj945  35175  bnj556  35301  bnj557  35302  bnj607  35317  bnj864  35323  bnj969  35347  bnj999  35359  bnj1398  35435  kardexen  35588  wevgblacfn  35607  elpotr  36283  dfon2lem8  36292  txpss3v  36380  meran1  36954  arg-ax  36959  bj-sbcex  37305  bj-nfalt  37370  bj-imdirco  37866  difunieq  38052  pibt1  38094  wl-cbvmotv  38200  poimirlem25  38328  poimirlem30  38333  bndss  38469  fldcrngo  38687  flddmn  38741  xrnss3v  39062  trressn  39216  redundss3  39393  redundpim3  39395  eldisjim  39568  eldisjim2  39569  eldisjn0el  39590  partim  39592  mainer  39629  prter1  39685  sn-sup2  43297  fimgmcyclem  43333  mzpclall  43490  setindtrs  43784  dgraalem  43904  oneptri  44016  ifpimim  44267  inintabss  44336  refimssco  44365  cotrintab  44372  intimass  44412  psshepw  44546  nzin  45060  axc11next  45148  iotaexeu  45160  hbexgVD  45646  orbitclmpt  45699  wfaxrep  45735  wfaxsep  45736  wfaxpow  45738  wfaxpr  45739  wfac8prim  45743  permaxinf2lem  45753  absnsb  47796  aovpcov0  47959  aov0ov0  47962  muldvdsfacgt  48155  ichan  48236  ichal  48247  spr0el  48263  sprsymrelf  48276  enege  48442  onego  48443  gbogbow  48553  gpgvtxedg0  48860  gpgvtxedg1  48861  gpgprismgr4cycllem10  48901  sgrpplusgaopALT  48992  rhmsubcALTVlem3  49080  eluz2cnn0n1  49323  regt1loggt0  49348  rege1logbrege0  49370  rege1logbzge0  49371  relogbmulbexp  49373  islan2  50436  alseuals  50634  ralseurals  50635