Theorem 3imtr4i 292

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  hbxfrbi  1827  excomimw  2046  nexmo  2541  eu6im  2575  ralimi2  3069  reximi2  3070  rabid2im  3421  elexOLD  3451  rmoan  3685  rmoimi2  3689  reuan  3834  sstr2  3928  rabss2OLD  4018  n0rex  4297  undif4  4407  rzal  4434  difprsnss  4744  snsspw  4787  uniin  4874  iuniin  4946  iuneq1  4950  iuneq2  4953  iunpwss  5049  axrep6  5221  axrep6OLD  5222  eunex  5332  rmorabex  5412  exss  5415  soeq2  5561  reliin  5773  coeq1  5812  coeq2  5813  cnveq  5828  dmeq  5858  dmin  5866  dmcoss  5930  dmcossOLD  5931  rncoeq  5937  dminss  6117  imainss  6118  dfco2a  6210  fundif  6547  fununi  6573  fof  6752  f1ocnv  6792  foco2  7061  isocnv  7285  isotr  7291  oprabidw  7398  oprabid  7399  zfrep6OLD  7908  ovmptss  8043  dmtpos  8188  tposfn  8205  smores  8292  omopthlem1  8595  brinxper  8673  eqer  8680  fsetsspwxp  8800  ixpeq2  8859  enssdomOLD  8924  fiprc  8991  sbthlem9  9033  infensuc  9093  fipwuni  9339  dfom3  9568  ttrcltr  9637  r1elss  9730  scott0  9810  fin56  10315  dominf  10367  ac6n  10407  brdom4  10452  dominfac  10496  inawina  10613  eltsk2g  10674  ltsosr  11017  ssxr  11215  recgt0ii  12062  sup2  12112  dfnn2  12187  peano2uz2  12617  eluzp1p1  12816  peano2uz  12851  ubmelfzo  13685  elfzlmr  13737  expclzlem  14045  wrdeq  14498  wwlktovf  14918  fsum2dlem  15732  fprod2dlem  15945  sin02gt0  16159  divalglem6  16367  qredeu  16627  isfunc  17831  xpcbas  18144  drsdirfi  18271  clatl  18474  tsrss  18555  mhmismgmhm  18759  smndex1mgm  18878  gimcnv  19242  gsum2dlem1  19945  gsum2dlem2  19946  rhmisrnghm  20460  subrngrng  20527  srhmsubclem1  20654  fldidom  20748  lmimcnv  21062  xrge0subm  21423  fctop  22969  cctop  22971  alexsubALTlem4  24015  lpbl  24468  xrge0gsumle  24799  xrge0tsms  24800  iirev  24896  iihalf1  24898  iihalf2  24900  iimulcl  24904  vitalilem1  25575  ply1idom  26090  aacjcl  26293  aannenlem2  26295  ang180lem4  26776  lgslem3  27262  ltsval2  27620  madef  27828  lrrecfr  27935  norecdiv  28182  elons2  28250  dfn0s2  28324  nnaddscl  28338  nnmulscl  28339  znegscl  28384  uzsind  28397  zsoring  28401  z12negscl  28470  renegscl  28490  readdscl  28491  remulscl  28494  tgjustf  28541  axlowdim  29030  axcontlem2  29034  usgrexmplef  29328  cusgrop  29507  rusgrpropedg  29653  spthispth  29792  pthdifv  29798  cycliscrct  29867  wwlksn0  29931  clwwlkccat  30060  clwwlkn  30096  clwwlknonccat  30166  numclwwlk1  30431  nmobndseqi  30850  axhcompl-zf  31069  hhcmpl  31271  shunssi  31439  spansni  31628  pjoml3i  31657  cmcmlem  31662  nonbooli  31722  lnopco0i  32075  pjnmopi  32219  pjnormssi  32239  hatomistici  32433  cvexchi  32440  cmdmdi  32488  mddmdin0i  32502  cdj3lem3b  32511  rmoun  32563  disjin  32656  disjin2  32657  xrge0tsmsd  33134  issgon  34267  sxbrsigalem0  34415  eulerpartlemgs2  34524  ballotlem2  34633  ballotth  34682  bnj945  34916  bnj556  35042  bnj557  35043  bnj607  35058  bnj864  35064  bnj969  35088  bnj999  35100  bnj1398  35176  wevgblacfn  35291  elpotr  35961  dfon2lem8  35970  txpss3v  36058  meran1  36593  arg-ax  36598  bj-sbcex  36945  bj-nfalt  37010  bj-imdirco  37504  difunieq  37690  pibt1  37732  wl-cbvmotv  37838  poimirlem25  37966  poimirlem30  37971  bndss  38107  fldcrngo  38325  flddmn  38379  xrnss3v  38702  trressn  38856  redundss3  39033  redundpim3  39035  eldisjim  39208  eldisjim2  39209  eldisjn0el  39230  partim  39232  mainer  39269  prter1  39325  sn-sup2  42936  rimcnv  42962  fimgmcyclem  42978  mzpclall  43159  setindtrs  43453  dgraalem  43573  oneptri  43685  ifpimim  43936  inintabss  44005  refimssco  44034  cotrintab  44041  intimass  44081  psshepw  44215  nzin  44745  axc11next  44833  iotaexeu  44845  hbexgVD  45332  orbitclmpt  45385  wfaxrep  45421  wfaxsep  45422  wfaxpow  45424  wfaxpr  45425  wfac8prim  45429  permaxinf2lem  45439  absnsb  47475  aovpcov0  47638  aov0ov0  47641  muldvdsfacgt  47834  ichan  47915  ichal  47926  spr0el  47942  sprsymrelf  47955  enege  48121  onego  48122  gbogbow  48232  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgprismgr4cycllem10  48580  sgrpplusgaopALT  48671  rhmsubcALTVlem3  48759  eluz2cnn0n1  48987  regt1loggt0  49012  rege1logbrege0  49034  rege1logbzge0  49035  relogbmulbexp  49037  islan2  50101