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:  hbxfrbi  1827  nexmo  2534  moimi  2538  eu6im  2568  ralimi2  3077  reximi2  3078  rexbiOLD  3104  elex  3464  rmoan  3700  rmoimi2  3704  reuan  3855  sseq2  3973  rabss2  4040  n0rex  4319  undif4  4431  r19.2zb  4458  rzal  4471  difprsnss  4764  snsspw  4807  uniin  4897  iuniin  4971  iuneq1  4975  iuneq2  4978  iunpwss  5072  axrep6  5254  eunex  5350  rmorabex  5422  exss  5425  soeq2  5572  elopaelxpOLD  5727  reliin  5778  coeq1  5818  coeq2  5819  cnveq  5834  dmeq  5864  dmin  5872  dmcoss  5931  rncoeq  5935  dminss  6110  imainss  6111  dfco2a  6203  iotaexOLD  6481  fundif  6555  fununi  6581  fof  6761  f1ocnv  6801  foco2  7062  isocnv  7280  isotr  7286  oprabidw  7393  oprabid  7394  zfrep6  7892  ovmptss  8030  dmtpos  8174  tposfn  8191  smores  8303  omopthlem1  8610  eqer  8690  fsetsspwxp  8798  ixpeq2  8856  enssdom  8924  fiprc  8996  sbthlem9  9042  infensuc  9106  fipwuni  9371  dfom3  9592  ttrcltr  9661  r1elss  9751  scott0  9831  fin56  10338  dominf  10390  ac6n  10430  brdom4  10475  dominfac  10518  inawina  10635  eltsk2g  10696  ltsosr  11039  ssxr  11233  recgt0ii  12070  sup2  12120  dfnn2  12175  peano2uz2  12600  eluzp1p1  12800  peano2uz  12835  ubmelfzo  13647  elfzlmr  13696  expclzlem  13999  wrdeq  14436  wwlktovf  14857  fsum2dlem  15666  fprod2dlem  15874  sin02gt0  16085  divalglem6  16291  qredeu  16545  isfunc  17764  xpcbas  18080  drsdirfi  18208  clatl  18411  tsrss  18492  smndex1mgm  18731  gimcnv  19071  gsum2dlem1  19761  gsum2dlem2  19762  lmimcnv  20585  fldidom  20812  xrge0subm  20875  fctop  22391  cctop  22393  alexsubALTlem4  23438  lpbl  23896  xrge0gsumle  24233  xrge0tsms  24234  iirev  24329  iihalf1  24331  iihalf2  24333  iimulcl  24337  vitalilem1  25009  ply1idom  25526  aacjcl  25724  aannenlem2  25726  ang180lem4  26199  lgslem3  26684  sltval2  27041  madef  27229  lrrecfr  27298  tgjustf  27478  axlowdim  27973  axcontlem2  27977  usgrexmplef  28270  cusgrop  28449  rusgrpropedg  28595  spthispth  28737  cycliscrct  28810  wwlksn0  28871  clwwlkccat  28997  clwwlkn  29033  clwwlknonccat  29103  numclwwlk1  29368  nmobndseqi  29784  axhcompl-zf  30003  hhcmpl  30205  shunssi  30373  spansni  30562  pjoml3i  30591  cmcmlem  30596  nonbooli  30656  lnopco0i  31009  pjnmopi  31153  pjnormssi  31173  hatomistici  31367  cvexchi  31374  cmdmdi  31422  mddmdin0i  31436  cdj3lem3b  31445  rmoun  31486  disjin  31571  disjin2  31572  xrge0tsmsd  31969  issgon  32811  sxbrsigalem0  32960  eulerpartlemgs2  33069  ballotlem2  33177  ballotth  33226  bnj945  33474  bnj556  33601  bnj557  33602  bnj607  33617  bnj864  33623  bnj969  33647  bnj999  33659  bnj1398  33735  elpotr  34442  dfon2lem8  34451  txpss3v  34539  meran1  34959  arg-ax  34964  bj-nfalt  35252  bj-imdirco  35734  difunieq  35918  pibt1  35960  wl-cbvmotv  36045  poimirlem25  36176  poimirlem30  36181  bndss  36318  fldcrngo  36536  flddmn  36590  xrnss3v  36907  trressn  36980  redundss3  37163  redundpim3  37165  eldisjim  37319  eldisjim2  37320  eldisjn0el  37341  partim  37343  mainer  37369  prter1  37414  rimcnv  40765  sn-sup2  40996  mzpclall  41108  setindtrs  41407  dgraalem  41530  oneptri  41649  ifpimim  41903  inintabss  41972  refimssco  42001  cotrintab  42008  intimass  42048  psshepw  42182  nzin  42720  axc11next  42808  iotaexeu  42820  hbexgVD  43310  absnsb  45381  aovpcov0  45542  aov0ov0  45545  ichan  45767  ichal  45778  spr0el  45794  sprsymrelf  45807  enege  45957  onego  45958  gbogbow  46068  mhmismgmhm  46220  sgrpplusgaopALT  46249  rhmisrnghm  46338  srhmsubclem1  46491  rhmsubcALTVlem3  46524  eluz2cnn0n1  46712  regt1loggt0  46742  rege1logbrege0  46764  rege1logbzge0  46765  relogbmulbexp  46767