Theorem imbitrrid 246

Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)

Hypotheses

Ref	Expression
imbitrrid.1	⊢ (𝜑 → 𝜃)
imbitrrid.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
imbitrrid	⊢ (𝜒 → (𝜑 → 𝜓))

Proof of Theorem imbitrrid

Step	Hyp	Ref	Expression
1		imbitrrid.1	. 2 ⊢ (𝜑 → 𝜃)
2		imbitrrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	2	bicomd 223	. 2 ⊢ (𝜒 → (𝜃 ↔ 𝜓))
4	1, 3	imbitrid 244	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:  syl5ibrcom  247  biimprd  248  exdistrf  2452  pm2.61ne  3018  spcimgft  3492  unineq  4229  elpreqprlem  4810  oteqex  5446  otel3xp  5668  eqrelrdv2  5742  breldmg  5856  elrnmpt1  5907  cnveqb  6152  cnveq0  6153  predpoirr  6289  predfrirr  6290  limelon  6380  f1ssf1  6804  ndmfv  6864  eqfnun  6981  ffvresb  7070  isomin  7283  isofrlem  7286  oprabidw  7389  caovord3d  7568  eldifpw  7713  ssonuni  7725  onsucuni2  7776  ordzsl  7787  tfindsg  7803  findsg  7839  oteqimp  7952  frxp  8067  poxp  8069  fnwelem  8072  tfrlem11  8318  ord1eln01  8422  ord2eln012  8423  oacl  8461  omcl  8462  oecl  8463  oa0r  8464  om0r  8465  om1r  8469  oe1m  8471  oaordi  8472  oawordri  8476  oaass  8487  oarec  8488  omwordri  8498  odi  8505  omass  8506  oewordri  8519  oeworde  8520  oeordsuc  8521  oelim2  8522  oeoa  8524  oeoelem  8525  oeoe  8526  nnm0r  8537  nnacl  8538  nnacom  8544  nnaordi  8545  nnaass  8549  nndi  8550  nnmass  8551  nnmsucr  8552  nnmcom  8553  omabs  8578  brecop  8748  eceqoveq  8760  elpm2r  8783  map0g  8823  undifixp  8873  fundmen  8969  mapxpen  9072  mapunen  9075  pssnn  9094  php  9132  unxpdomlem2  9158  f1vrnfibi  9243  elfir  9319  wemapso2lem  9458  wdompwdom  9484  inf3lem1  9538  inf3lem3  9540  cantnfval2  9579  cantnfp1lem3  9590  r1sdom  9687  r1tr  9689  carden2a  9879  fidomtri2  9907  prdom2  9917  infxpenlem  9924  acndom  9962  fodomacn  9967  wdomfil  9972  alephon  9980  alephordi  9985  alephle  9999  alephfplem3  10017  dfac2a  10041  kmlem9  10070  cflm  10161  cfslb  10177  cfslbn  10178  infpssrlem3  10216  infpssrlem4  10217  fin23lem21  10250  fin23lem30  10253  isf34lem7  10290  isf34lem6  10291  fin67  10306  isfin7-2  10307  fin1a2lem7  10317  fin1a2lem10  10320  iundom2g  10451  konigthlem  10480  alephreg  10494  gchdomtri  10541  wunr1om  10631  tskr1om  10679  inar1  10687  grur1a  10731  indpi  10819  genpprecl  10913  genpnmax  10919  addcmpblnr  10981  recexsrlem  11015  map2psrpr  11022  ax1rid  11073  axpre-mulgt0  11080  ltle  11222  nnmulcl  12170  nnsub  12190  nn0sub  12452  nneo  12577  uz11  12777  xrltle  13064  xltnegi  13132  xrsupsslem  13223  xrinfmsslem  13224  xrub  13228  supxrunb1  13235  supxrunb2  13236  om2uzuzi  13873  uzrdgxfr  13891  seqcl2  13944  seqfveq2  13948  seqshft2  13952  seqsplit  13959  seqcaopr3  13961  seqf1olem2a  13964  seqid2  13972  seqhomo  13973  ser1const  13982  m1expcl2  14009  expadd  14028  expmul  14031  faclbnd  14214  hashfzp1  14355  hashmap  14359  hashf1lem2  14380  hashf1  14381  seqcoll  14388  wrdsymb0  14473  len0nnbi  14475  eqs1  14537  swrdnd2  14580  wrd2ind  14647  pfxccatin12lem2c  14654  pfxccatin12lem2  14655  swrdccatin1d  14667  repswccat  14710  repswcshw  14736  cshwcshid  14751  rtrclreclem3  14984  rtrclreclem4  14985  dfrtrcl2  14986  relexpindlem  14987  relexpind  14988  rtrclind  14989  recan  15261  rexanre  15271  rlimcn3  15514  caurcvg2  15602  fsumiun  15745  efexp  16027  rpnnen2lem12  16151  dvdstr  16222  alzdvds  16248  zob  16287  sumeven  16315  sumodd  16316  bitsinv1  16370  smu01lem  16413  smupval  16416  smueqlem  16418  smumullem  16420  seq1st  16499  lcmfunsnlem2lem1  16566  lcmfunsnlem2lem2  16567  cncongr2  16596  prmdiveq  16714  odzdvds  16724  pythagtriplem2  16746  pcexp  16788  vdwlem13  16922  ramz  16954  prmolefac  16975  elrestr  17349  xpsff1o  17489  subsubc  17778  clatl  18432  frmdgsum  18788  sursubmefmnd  18822  injsubmefmnd  18823  smndex1mndlem  18838  dfgrp3e  18974  mulgneg2  19042  mulgnnass  19043  mhmmulg  19049  gsumwrev  19299  symgextf1lem  19353  symgfixelsi  19368  pmtrdifellem4  19412  sylow1lem1  19531  efgsfo  19672  efgred  19681  cyggexb  19832  gsumzres  19842  gsum2dlem2  19904  mulgass2  20248  rngimcnv  20394  funcrngcsetc  20575  funcrngcsetcALT  20576  rhmsscrnghm  20600  funcringcsetc  20609  lmodprop2d  20877  lspsnne2  21075  lspsneu  21080  cnfldmulg  21360  cnfldexp  21361  zrhpsgnelbas  21551  assapropd  21828  mplcoe1  21993  mplcoe3  21994  mplcoe5  21996  mhpvarcl  22092  ply1sclf1  22232  mat1scmat  22482  restopn2  23120  cnpf2  23193  cmpfi  23351  txcn  23569  txlm  23591  xkoptsub  23597  xkopjcn  23599  ufildr  23874  cnflf  23945  fclsnei  23962  fclscmp  23973  ufilcmp  23975  cnfcf  23985  symgtgp  24049  isxms2  24391  met2ndc  24466  metustbl  24509  tngngp2  24595  clmmulg  25046  iscau4  25224  ovolunlem1a  25441  ovolicc2lem4  25465  volfiniun  25492  voliunlem1  25495  volsup  25501  dvnadd  25874  dvnres  25876  dvcobr  25891  ply1nzb  26069  plypf1  26158  dgrle  26189  coeaddlem  26195  dgrlt  26212  dvntaylp  26319  cxpmul2  26638  rlimcnp  26915  facgam  27016  wilthlem2  27019  isnsqf  27085  musum  27141  chtub  27163  chpval2  27169  gausslemma2dlem0i  27315  dchrisumlem1  27440  qabvexp  27577  ostthlem2  27579  nodenselem8  27643  lesrec  27779  bday1  27794  sltsleft  27840  sltsright  27841  oncutlt  28244  noseqind  28272  dfnns2  28352  bdaypw2n0bnd  28444  axsegconlem1  28974  ax5seglem4  28989  ax5seglem5  28990  axlowdimlem15  29013  axcontlem2  29022  axcontlem4  29024  incistruhgr  29136  upgredg2vtx  29198  upgredgpr  29199  numedglnl  29201  uhgr2edg  29265  nbupgruvtxres  29464  cusgrfilem1  29513  wlkres  29726  wlkp1lem2  29730  pthdivtx  29784  pthdlem2lem  29824  wlkiswwlks2lem4  29929  wwlksnredwwlkn0  29953  wwlksnextwrd  29954  wwlksnfi  29963  wwlksnextprop  29969  clwlkclwwlklem2a  30057  clwlkclwwlkf1lem2  30064  erclwwlksym  30080  clwwlkf1  30108  eleclclwwlknlem2  30120  erclwwlknsym  30129  clwwlknonex2  30168  eupth2lem3lem6  30292  frgr3vlem1  30332  3vfriswmgrlem  30336  wlkl0  30426  sspval  30783  nmosetre  30824  nmobndseqi  30839  nmobndseqiALT  30840  orthcom  31168  shsva  31380  shmodsi  31449  h1datomi  31641  nmopsetretALT  31923  nmfnsetre  31937  lnopcnbd  32096  pjclem4  32259  pj3si  32267  ssmd1  32371  atom1d  32413  chjatom  32417  atcvat4i  32457  cdj3lem2a  32496  cdj3lem3a  32499  disjunsn  32653  unitdivcld  34051  xrge0iifiso  34085  dya2iocuni  34433  bnj168  34879  bnj535  35038  bnj590  35058  bnj594  35060  bnj938  35085  bnj1118  35132  bnj1128  35138  fnrelpredd  35240  deranglem  35354  subfacp1lem6  35373  subfacval2  35375  cvmlift2lem12  35502  satffun  35597  mrsubvrs  35710  msrrcl  35731  mclsax  35757  dfon2lem6  35974  rdgprc  35980  ifscgr  36232  btwncolinear1  36257  hfelhf  36369  opnrebl2  36509  nn0prpw  36511  ordcmp  36635  findreccl  36641  nndivlub  36646  axtcond  36666  dfttc2g  36694  bj-rest0  37403  bj-isrvec2  37612  topdifinffinlem  37659  iooelexlt  37674  rdgeqoa  37682  exrecfnlem  37691  wl-mo3t  37892  matunitlindflem2  37929  poimirlem2  37934  poimirlem23  37955  poimirlem28  37960  poimirlem29  37961  poimirlem31  37963  poimirlem32  37964  sdclem2  38054  sdclem1  38055  prdsbnd2  38107  ismtyval  38112  rrnequiv  38147  isexid2  38167  ismndo1  38185  exidreslem  38189  rngo2  38219  rngoueqz  38252  risci  38299  eldisjdmqsim  39129  prtlem11  39303  prtlem15  39312  cvrat4  39880  lcfl6  41937  dvdsexpnn0  42765  harval3  43968  clcnvlem  44053  cnvrcl0  44055  cnvtrcl0  44056  iunrelexpmin1  44138  iunrelexpmin2  44142  ormkglobd  47307  fcoresf1b  47504  aovmpt4g  47635  elsetpreimafvbi  47825  iccpartiltu  47856  iccpartgt  47861  iccpartgel  47863  reuopreuprim  47960  fmtnofac1  48004  gbepos  48192  grtrif1o  48376  grtriclwlk3  48379  isubgr3stgrlem4  48403  gpgprismgr4cycllem3  48531  pgnbgreunbgrlem1  48547  pgnbgreunbgrlem3  48552  pgnbgreunbgrlem4  48553  pgnbgreunbgrlem5lem1  48554  pgnbgreunbgrlem5lem2  48555  pgnbgreunbgrlem5lem3  48556  pgnbgreunbgrlem6  48558  pgnbgreunbgr  48559  ellcoellss  48869  dignn0flhalflem2  49050  nn0sumshdiglemB  49054  1arympt1  49072  opth1neg  49259  opth2neg  49260  oppccatb  49449  fullthinc  49883