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  1857  excomimw  2078  nexmo  2569  eu6im  2603  ralimi2  3097  reximi2  3098  rabid2im  3446  rmoan  3699  rmoimi2  3703  reuan  3847  sstr2  3919  rabss2OLD  4005  n0rex  4307  undif4  4422  rzal  4452  difprsnss  4761  snsspw  4801  uniinOLD  4894  iuniin  4966  iuneq1  4970  iuneq2  4973  iunpwss  5069  axrep6  5242  eunex  5355  rmorabex  5431  exss  5434  soeq2  5584  reliin  5799  coeq1  5839  coeq2  5840  cnveq  5855  dmeq  5889  dmin  5897  dmcoss  5961  dmcossOLD  5962  rncoeq  5967  dminss  6148  imainss  6149  dfco2a  6253  fundif  6597  fununi  6623  fof  6804  f1ocnv  6845  foco2  7117  isocnv  7345  isotr  7351  oprabidw  7458  oprabid  7459  zfrep6OLD  7974  ovmptssOLD  8113  dmtpos  8266  tposfn  8283  smores  8371  omopthlem1  8679  brinxper  8758  eqer  8765  fsetsspwxp  8886  ixpeq2  8950  enssdomOLD  9015  fiprc  9083  sbthlem9  9125  infensuc  9185  fipwuni  9428  dfom3  9658  ttrcltr  9727  r1elss  9824  scott0b  9947  scott0OLD  9948  fin56  10481  dominf  10533  ac6n  10573  brdom4  10619  dominfac  10668  inawina  10785  eltsk2g  10846  ltsosr  11189  ssxr  11389  recgt0ii  12233  sup2  12283  dfnn2  12358  peano2uz2  12797  eluzp1p1  13003  peano2uz  13038  ubmelfzo  13875  elfzlmr  13927  expclzlem  14236  wrdeq  14691  wwlktovf  15121  fsum2dlem  15948  fprod2dlem  16159  sin02gt0  16372  divalglem6  16580  qredeu  16845  isfunc  18051  xpcbas  18364  drsdirfi  18491  clatl  18694  tsrss  18775  mhmismgmhm  18998  smndex1mgm  19118  gimcnv  19493  gsum2dlem1  20196  gsum2dlem2  20197  rhmisrnghm  20723  rimcnv  20729  subrngrng  20814  srhmsubclem1  20941  fldidom  21041  lmimcnv  21354  xrge0subm  21761  fctop  23334  cctop  23336  alexsubALTlem4  24381  lpbl  24834  xrge0gsumle  25165  xrge0tsms  25166  iirev  25262  iihalf1  25264  iihalf2  25266  iimulcl  25270  vitalilem1  25941  ply1idom  26455  aacjcl  26666  aannenlem2  26668  ang180lem4  27152  lgslem3  27638  ltsval2  28025  madef  28234  lrrecfr  28341  norecdiv  28588  elons2  28656  dfn0s2  28730  nnaddscl  28744  nnmulscl  28745  znegscl  28790  uzsind  28803  zsoring  28807  z12negscl  28876  renegscl  28896  readdscl  28897  remulscl  28900  tgjustf  28947  axlowdim  29551  axcontlem2  29555  usgrexmplef  29852  cusgrop  30031  rusgrpropedg  30177  spthispth  30321  pthdifv  30328  cycliscrct  30399  wwlksn0  30464  clwwlkccat  30593  clwwlkn  30629  clwwlknonccat  30699  numclwwlk1  30974  nmobndseqi  31393  axhcompl-zf  31612  hhcmpl  31814  shunssi  31982  spansni  32171  pjoml3i  32200  cmcmlem  32205  nonbooli  32265  lnopco0i  32618  pjnmopi  32762  pjnormssi  32782  hatomistici  32976  cvexchi  32983  cmdmdi  33031  mddmdin0i  33045  cdj3lem3b  33054  rmoun  33144  disjin  33234  disjin2  33235  xrge0tsmsd  33687  issgon  34808  sxbrsigalem0  34956  eulerpartlemgs2  35065  ballotlem2  35174  ballotth  35223  bnj945  35457  bnj556  35583  bnj557  35584  bnj607  35599  bnj864  35605  bnj969  35629  bnj999  35641  bnj1398  35717  rankse  35802  kardexen  35902  wevgblacfn  35993  vsmrep  36044  elpotr  36670  dfon2lem8  36679  txpss3v  36767  meran1  37326  arg-ax  37331  bj-sbcex  37677  bj-nfalt  37742  bj-imdirco  38251  difunieq  38437  pibt1  38479  wl-cbvmotv  38585  poimirlem25  38703  poimirlem30  38708  bndss  38860  fldcrngo  39078  flddmn  39132  xrnss3v  39453  trressn  39607  redundss3  39784  redundpim3  39786  eldisjim  39959  eldisjim2  39960  eldisjn0el  39981  partim  39983  mainer  40020  prter1  40076  sn-sup2  43695  fimgmcyclem  43737  mzpclall  43878  setindtrs  44172  dgraalem  44287  oneptri  44399  ifpimim  44650  inintabss  44719  refimssco  44747  cotrintab  44754  intimass  44794  psshepw  44928  nzin  45442  axc11next  45530  iotaexeu  45541  hbexgVD  46027  orbitclmpt  46087  wfaxrep  46123  wfaxsep  46124  wfaxpow  46126  wfaxpr  46127  wfac8prim  46131  permaxinf2lem  46141  absnsb  48236  aovpcov0  48399  aov0ov0  48402  muldvdsfacgt  48595  ichan  48676  ichal  48687  spr0el  48703  sprsymrelf  48716  enege  48882  onego  48883  gbogbow  48993  gpgvtxedg0  49300  gpgvtxedg1  49301  gpgprismgr4cycllem10  49341  sgrpplusgaopALT  49431  rhmsubcALTVlem3  49519  eluz2cnn0n1  49762  regt1loggt0  49787  rege1logbrege0  49809  rege1logbzge0  49810  relogbmulbexp  49812  islan2  50948  alseuals  51134  ralseurals  51135