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  2567  eu6im  2601  ralimi2  3095  reximi2  3096  rabid2im  3444  rmoan  3697  rmoimi2  3701  reuan  3844  sstr2  3938  rabss2OLD  4026  n0rex  4305  undif4  4420  rzal  4450  difprsnss  4762  snsspw  4804  uniinOLD  4892  iuniin  4964  iuneq1  4968  iuneq2  4971  iunpwss  5067  axrep6  5240  eunex  5352  rmorabex  5428  exss  5431  soeq2  5581  reliin  5795  coeq1  5835  coeq2  5836  cnveq  5851  dmeq  5885  dmin  5893  dmcoss  5957  dmcossOLD  5958  rncoeq  5963  dminss  6143  imainss  6144  dfco2a  6247  fundif  6589  fununi  6615  fof  6796  f1ocnv  6837  foco2  7109  isocnv  7338  isotr  7344  oprabidw  7451  oprabid  7452  zfrep6OLD  7967  ovmptss  8104  dmtpos  8255  tposfn  8272  smores  8360  omopthlem1  8668  brinxper  8747  eqer  8754  fsetsspwxp  8875  ixpeq2  8939  enssdomOLD  9004  fiprc  9072  sbthlem9  9114  infensuc  9174  fipwuni  9418  dfom3  9648  ttrcltr  9717  r1elss  9814  scott0b  9937  scott0OLD  9938  fin56  10471  dominf  10523  ac6n  10563  brdom4  10609  dominfac  10658  inawina  10775  eltsk2g  10836  ltsosr  11179  ssxr  11379  recgt0ii  12223  sup2  12273  dfnn2  12348  peano2uz2  12787  eluzp1p1  12993  peano2uz  13028  ubmelfzo  13865  elfzlmr  13917  expclzlem  14226  wrdeq  14681  wwlktovf  15109  fsum2dlem  15936  fprod2dlem  16147  sin02gt0  16360  divalglem6  16568  qredeu  16833  isfunc  18039  xpcbas  18352  drsdirfi  18479  clatl  18682  tsrss  18763  mhmismgmhm  18986  smndex1mgm  19106  gimcnv  19481  gsum2dlem1  20184  gsum2dlem2  20185  rhmisrnghm  20711  rimcnv  20717  subrngrng  20802  srhmsubclem1  20929  fldidom  21029  lmimcnv  21342  xrge0subm  21749  fctop  23322  cctop  23324  alexsubALTlem4  24369  lpbl  24822  xrge0gsumle  25153  xrge0tsms  25154  iirev  25250  iihalf1  25252  iihalf2  25254  iimulcl  25258  vitalilem1  25929  ply1idom  26443  aacjcl  26654  aannenlem2  26656  ang180lem4  27140  lgslem3  27626  ltsval2  28013  madef  28222  lrrecfr  28329  norecdiv  28576  elons2  28644  dfn0s2  28718  nnaddscl  28732  nnmulscl  28733  znegscl  28778  uzsind  28791  zsoring  28795  z12negscl  28864  renegscl  28884  readdscl  28885  remulscl  28888  tgjustf  28935  axlowdim  29539  axcontlem2  29543  usgrexmplef  29840  cusgrop  30019  rusgrpropedg  30165  spthispth  30309  pthdifv  30316  cycliscrct  30387  wwlksn0  30452  clwwlkccat  30581  clwwlkn  30617  clwwlknonccat  30687  numclwwlk1  30962  nmobndseqi  31381  axhcompl-zf  31600  hhcmpl  31802  shunssi  31970  spansni  32159  pjoml3i  32188  cmcmlem  32193  nonbooli  32253  lnopco0i  32606  pjnmopi  32750  pjnormssi  32770  hatomistici  32964  cvexchi  32971  cmdmdi  33019  mddmdin0i  33033  cdj3lem3b  33042  rmoun  33090  disjin  33180  disjin2  33181  xrge0tsmsd  33634  issgon  34755  sxbrsigalem0  34903  eulerpartlemgs2  35012  ballotlem2  35121  ballotth  35170  bnj945  35404  bnj556  35530  bnj557  35531  bnj607  35546  bnj864  35552  bnj969  35576  bnj999  35588  bnj1398  35664  kardexen  35831  wevgblacfn  35890  elpotr  36543  dfon2lem8  36552  txpss3v  36640  meran1  37199  arg-ax  37204  bj-sbcex  37550  bj-nfalt  37615  bj-imdirco  38111  difunieq  38297  pibt1  38339  wl-cbvmotv  38445  poimirlem25  38563  poimirlem30  38568  bndss  38720  fldcrngo  38938  flddmn  38992  xrnss3v  39313  trressn  39467  redundss3  39644  redundpim3  39646  eldisjim  39819  eldisjim2  39820  eldisjn0el  39841  partim  39843  mainer  39880  prter1  39936  sn-sup2  43555  fimgmcyclem  43597  mzpclall  43737  setindtrs  44031  dgraalem  44146  oneptri  44258  ifpimim  44509  inintabss  44578  refimssco  44606  cotrintab  44613  intimass  44653  psshepw  44787  nzin  45301  axc11next  45389  iotaexeu  45401  hbexgVD  45887  orbitclmpt  45947  wfaxrep  45983  wfaxsep  45984  wfaxpow  45986  wfaxpr  45987  wfac8prim  45991  permaxinf2lem  46001  absnsb  48096  aovpcov0  48259  aov0ov0  48262  muldvdsfacgt  48455  ichan  48536  ichal  48547  spr0el  48563  sprsymrelf  48576  enege  48742  onego  48743  gbogbow  48853  gpgvtxedg0  49160  gpgvtxedg1  49161  gpgprismgr4cycllem10  49201  sgrpplusgaopALT  49291  rhmsubcALTVlem3  49379  eluz2cnn0n1  49622  regt1loggt0  49647  rege1logbrege0  49669  rege1logbzge0  49670  relogbmulbexp  49672  islan2  50733  alseuals  50919  ralseurals  50920