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  2571  eu6im  2605  ralimi2  3099  reximi2  3100  rabid2im  3450  rmoan  3704  rmoimi2  3708  reuan  3851  sstr2  3945  rabss2OLD  4033  n0rex  4312  undif4  4427  rzal  4457  difprsnss  4769  snsspw  4811  uniinOLD  4899  iuniin  4971  iuneq1  4975  iuneq2  4978  iunpwss  5075  axrep6  5249  axrep6OLD  5250  eunex  5363  rmorabex  5443  exss  5446  soeq2  5593  reliin  5806  coeq1  5845  coeq2  5846  cnveq  5861  dmeq  5895  dmin  5903  dmcoss  5967  dmcossOLD  5968  rncoeq  5973  dminss  6152  imainss  6153  dfco2a  6249  fundif  6589  fununi  6615  fof  6796  f1ocnv  6837  foco2  7108  isocnv  7337  isotr  7343  oprabidw  7450  oprabid  7451  zfrep6OLD  7958  ovmptss  8094  dmtpos  8240  tposfn  8257  smores  8345  omopthlem1  8651  brinxper  8730  eqer  8737  fsetsspwxp  8856  ixpeq2  8915  enssdomOLD  8980  fiprc  9048  sbthlem9  9090  infensuc  9150  fipwuni  9393  dfom3  9623  ttrcltr  9692  r1elss  9785  scott0b  9873  scott0OLD  9874  fin56  10392  dominf  10444  ac6n  10484  brdom4  10529  dominfac  10575  inawina  10692  eltsk2g  10753  ltsosr  11096  ssxr  11296  recgt0ii  12138  sup2  12188  dfnn2  12263  peano2uz2  12702  eluzp1p1  12908  peano2uz  12943  ubmelfzo  13778  elfzlmr  13830  expclzlem  14139  wrdeq  14593  wwlktovf  15019  fsum2dlem  15846  fprod2dlem  16059  sin02gt0  16272  divalglem6  16480  qredeu  16740  isfunc  17945  xpcbas  18258  drsdirfi  18385  clatl  18588  tsrss  18669  mhmismgmhm  18888  smndex1mgm  19008  gimcnv  19383  gsum2dlem1  20086  gsum2dlem2  20087  rhmisrnghm  20611  rimcnv  20617  subrngrng  20701  srhmsubclem1  20828  fldidom  20927  lmimcnv  21240  xrge0subm  21645  fctop  23213  cctop  23215  alexsubALTlem4  24260  lpbl  24713  xrge0gsumle  25044  xrge0tsms  25045  iirev  25141  iihalf1  25143  iihalf2  25145  iimulcl  25149  vitalilem1  25820  ply1idom  26335  aacjcl  26543  aannenlem2  26545  ang180lem4  27030  lgslem3  27516  ltsval2  27873  madef  28082  lrrecfr  28189  norecdiv  28436  elons2  28504  dfn0s2  28578  nnaddscl  28592  nnmulscl  28593  znegscl  28638  uzsind  28651  zsoring  28655  z12negscl  28724  renegscl  28744  readdscl  28745  remulscl  28748  tgjustf  28795  axlowdim  29368  axcontlem2  29372  usgrexmplef  29669  cusgrop  29848  rusgrpropedg  29994  spthispth  30138  pthdifv  30145  cycliscrct  30216  wwlksn0  30281  clwwlkccat  30410  clwwlkn  30446  clwwlknonccat  30516  numclwwlk1  30785  nmobndseqi  31204  axhcompl-zf  31423  hhcmpl  31625  shunssi  31793  spansni  31982  pjoml3i  32011  cmcmlem  32016  nonbooli  32076  lnopco0i  32429  pjnmopi  32573  pjnormssi  32593  hatomistici  32787  cvexchi  32794  cmdmdi  32842  mddmdin0i  32856  cdj3lem3b  32865  rmoun  32913  disjin  33004  disjin2  33005  xrge0tsmsd  33459  issgon  34579  sxbrsigalem0  34728  eulerpartlemgs2  34837  ballotlem2  34946  ballotth  34995  bnj945  35229  bnj556  35355  bnj557  35356  bnj607  35371  bnj864  35377  bnj969  35401  bnj999  35413  bnj1398  35489  kardexen  35635  wevgblacfn  35654  elpotr  36310  dfon2lem8  36319  txpss3v  36407  meran1  36981  arg-ax  36986  bj-sbcex  37332  bj-nfalt  37397  bj-imdirco  37893  difunieq  38079  pibt1  38121  wl-cbvmotv  38227  poimirlem25  38355  poimirlem30  38360  bndss  38497  fldcrngo  38715  flddmn  38769  xrnss3v  39090  trressn  39244  redundss3  39421  redundpim3  39423  eldisjim  39596  eldisjim2  39597  eldisjn0el  39618  partim  39620  mainer  39657  prter1  39713  sn-sup2  43325  fimgmcyclem  43361  mzpclall  43518  setindtrs  43812  dgraalem  43932  oneptri  44044  ifpimim  44295  inintabss  44364  refimssco  44393  cotrintab  44400  intimass  44440  psshepw  44574  nzin  45088  axc11next  45176  iotaexeu  45188  hbexgVD  45674  orbitclmpt  45727  wfaxrep  45763  wfaxsep  45764  wfaxpow  45766  wfaxpr  45767  wfac8prim  45771  permaxinf2lem  45781  absnsb  47824  aovpcov0  47987  aov0ov0  47990  muldvdsfacgt  48183  ichan  48264  ichal  48275  spr0el  48291  sprsymrelf  48304  enege  48470  onego  48471  gbogbow  48581  gpgvtxedg0  48888  gpgvtxedg1  48889  gpgprismgr4cycllem10  48929  sgrpplusgaopALT  49019  rhmsubcALTVlem3  49107  eluz2cnn0n1  49350  regt1loggt0  49375  rege1logbrege0  49397  rege1logbzge0  49398  relogbmulbexp  49400  islan2  50463  alseuals  50661  ralseurals  50662