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  2449  pm2.61ne  3014  spcimgft  3500  unineq  4237  elpreqprlem  4817  oteqex  5443  otel3xp  5665  eqrelrdv2  5739  breldmg  5853  elrnmpt1  5904  cnveqb  6148  cnveq0  6149  predpoirr  6285  predfrirr  6286  limelon  6376  f1ssf1  6800  ndmfv  6860  eqfnun  6976  ffvresb  7064  isomin  7277  isofrlem  7280  oprabidw  7383  caovord3d  7562  eldifpw  7707  ssonuni  7719  onsucuni2  7770  ordzsl  7781  tfindsg  7797  findsg  7833  oteqimp  7946  frxp  8062  poxp  8064  fnwelem  8067  tfrlem11  8313  ord1eln01  8417  ord2eln012  8418  oacl  8456  omcl  8457  oecl  8458  oa0r  8459  om0r  8460  om1r  8464  oe1m  8466  oaordi  8467  oawordri  8471  oaass  8482  oarec  8483  omwordri  8493  odi  8500  omass  8501  oewordri  8513  oeworde  8514  oeordsuc  8515  oelim2  8516  oeoa  8518  oeoelem  8519  oeoe  8520  nnm0r  8531  nnacl  8532  nnacom  8538  nnaordi  8539  nnaass  8543  nndi  8544  nnmass  8545  nnmsucr  8546  nnmcom  8547  omabs  8572  brecop  8740  eceqoveq  8752  elpm2r  8775  map0g  8814  undifixp  8864  fundmen  8960  mapxpen  9063  mapunen  9066  pssnn  9085  php  9123  unxpdomlem2  9148  f1vrnfibi  9233  elfir  9306  wemapso2lem  9445  wdompwdom  9471  inf3lem1  9525  inf3lem3  9527  cantnfval2  9566  cantnfp1lem3  9577  r1sdom  9674  r1tr  9676  carden2a  9866  fidomtri2  9894  prdom2  9904  infxpenlem  9911  acndom  9949  fodomacn  9954  wdomfil  9959  alephon  9967  alephordi  9972  alephle  9986  alephfplem3  10004  dfac2a  10028  kmlem9  10057  cflm  10148  cfslb  10164  cfslbn  10165  infpssrlem3  10203  infpssrlem4  10204  fin23lem21  10237  fin23lem30  10240  isf34lem7  10277  isf34lem6  10278  fin67  10293  isfin7-2  10294  fin1a2lem7  10304  fin1a2lem10  10307  iundom2g  10438  konigthlem  10466  alephreg  10480  gchdomtri  10527  wunr1om  10617  tskr1om  10665  inar1  10673  grur1a  10717  indpi  10805  genpprecl  10899  genpnmax  10905  addcmpblnr  10967  recexsrlem  11001  map2psrpr  11008  ax1rid  11059  axpre-mulgt0  11066  ltle  11208  nnmulcl  12156  nnsub  12176  nn0sub  12438  nneo  12563  uz11  12763  xrltle  13050  xltnegi  13117  xrsupsslem  13208  xrinfmsslem  13209  xrub  13213  supxrunb1  13220  supxrunb2  13221  om2uzuzi  13858  uzrdgxfr  13876  seqcl2  13929  seqfveq2  13933  seqshft2  13937  seqsplit  13944  seqcaopr3  13946  seqf1olem2a  13949  seqid2  13957  seqhomo  13958  ser1const  13967  m1expcl2  13994  expadd  14013  expmul  14016  faclbnd  14199  hashfzp1  14340  hashmap  14344  hashf1lem2  14365  hashf1  14366  seqcoll  14373  wrdsymb0  14458  len0nnbi  14460  eqs1  14522  swrdnd2  14565  wrd2ind  14632  pfxccatin12lem2c  14639  pfxccatin12lem2  14640  swrdccatin1d  14652  repswccat  14695  repswcshw  14721  cshwcshid  14736  rtrclreclem3  14969  rtrclreclem4  14970  dfrtrcl2  14971  relexpindlem  14972  relexpind  14973  rtrclind  14974  recan  15246  rexanre  15256  rlimcn3  15499  caurcvg2  15587  fsumiun  15730  efexp  16012  rpnnen2lem12  16136  dvdstr  16207  alzdvds  16233  zob  16272  sumeven  16300  sumodd  16301  bitsinv1  16355  smu01lem  16398  smupval  16401  smueqlem  16403  smumullem  16405  seq1st  16484  lcmfunsnlem2lem1  16551  lcmfunsnlem2lem2  16552  cncongr2  16581  prmdiveq  16699  odzdvds  16709  pythagtriplem2  16731  pcexp  16773  vdwlem13  16907  ramz  16939  prmolefac  16960  elrestr  17334  xpsff1o  17473  subsubc  17762  clatl  18416  frmdgsum  18772  sursubmefmnd  18806  injsubmefmnd  18807  smndex1mndlem  18819  dfgrp3e  18955  mulgneg2  19023  mulgnnass  19024  mhmmulg  19030  gsumwrev  19280  symgextf1lem  19334  symgfixelsi  19349  pmtrdifellem4  19393  sylow1lem1  19512  efgsfo  19653  efgred  19662  cyggexb  19813  gsumzres  19823  gsum2dlem2  19885  mulgass2  20229  rngimcnv  20376  funcrngcsetc  20557  funcrngcsetcALT  20558  rhmsscrnghm  20582  funcringcsetc  20591  lmodprop2d  20859  lspsnne2  21057  lspsneu  21062  cnfldmulg  21342  cnfldexp  21343  zrhpsgnelbas  21533  assapropd  21811  mplcoe1  21973  mplcoe3  21974  mplcoe5  21976  mhpvarcl  22064  ply1sclf1  22204  mat1scmat  22455  restopn2  23093  cnpf2  23166  cmpfi  23324  txcn  23542  txlm  23564  xkoptsub  23570  xkopjcn  23572  ufildr  23847  cnflf  23918  fclsnei  23935  fclscmp  23946  ufilcmp  23948  cnfcf  23958  symgtgp  24022  isxms2  24364  met2ndc  24439  metustbl  24482  tngngp2  24568  clmmulg  25029  iscau4  25207  ovolunlem1a  25425  ovolicc2lem4  25449  volfiniun  25476  voliunlem1  25479  volsup  25485  dvnadd  25859  dvnres  25861  dvcobr  25877  dvcobrOLD  25878  ply1nzb  26056  plypf1  26145  dgrle  26176  coeaddlem  26182  dgrlt  26200  dvntaylp  26307  cxpmul2  26626  rlimcnp  26903  facgam  27004  wilthlem2  27007  isnsqf  27073  musum  27129  chtub  27151  chpval2  27157  gausslemma2dlem0i  27303  dchrisumlem1  27428  qabvexp  27565  ostthlem2  27567  nodenselem8  27631  slerec  27761  bday1s  27776  ssltleft  27816  ssltright  27817  onscutlt  28202  noseqind  28223  dfnns2  28298  axsegconlem1  28897  ax5seglem4  28912  ax5seglem5  28913  axlowdimlem15  28936  axcontlem2  28945  axcontlem4  28947  incistruhgr  29059  upgredg2vtx  29121  upgredgpr  29122  numedglnl  29124  uhgr2edg  29188  nbupgruvtxres  29387  cusgrfilem1  29436  wlkres  29649  wlkp1lem2  29653  pthdivtx  29707  pthdlem2lem  29747  wlkiswwlks2lem4  29852  wwlksnredwwlkn0  29876  wwlksnextwrd  29877  wwlksnfi  29886  wwlksnextprop  29892  clwlkclwwlklem2a  29980  clwlkclwwlkf1lem2  29987  erclwwlksym  30003  clwwlkf1  30031  eleclclwwlknlem2  30043  erclwwlknsym  30052  clwwlknonex2  30091  eupth2lem3lem6  30215  frgr3vlem1  30255  3vfriswmgrlem  30259  wlkl0  30349  sspval  30705  nmosetre  30746  nmobndseqi  30761  nmobndseqiALT  30762  orthcom  31090  shsva  31302  shmodsi  31371  h1datomi  31563  nmopsetretALT  31845  nmfnsetre  31859  lnopcnbd  32018  pjclem4  32181  pj3si  32189  ssmd1  32293  atom1d  32335  chjatom  32339  atcvat4i  32379  cdj3lem2a  32418  cdj3lem3a  32421  disjunsn  32576  unitdivcld  33935  xrge0iifiso  33969  dya2iocuni  34317  bnj168  34763  bnj535  34923  bnj590  34943  bnj594  34945  bnj938  34970  bnj1118  35017  bnj1128  35023  fnrelpredd  35123  deranglem  35231  subfacp1lem6  35250  subfacval2  35252  cvmlift2lem12  35379  satffun  35474  mrsubvrs  35587  msrrcl  35608  mclsax  35634  dfon2lem6  35851  rdgprc  35857  ifscgr  36109  btwncolinear1  36134  hfelhf  36246  opnrebl2  36386  nn0prpw  36388  ordcmp  36512  findreccl  36518  nndivlub  36523  bj-rest0  37158  bj-isrvec2  37365  topdifinffinlem  37412  iooelexlt  37427  rdgeqoa  37435  exrecfnlem  37444  wl-mo3t  37641  matunitlindflem2  37677  poimirlem2  37682  poimirlem23  37703  poimirlem28  37708  poimirlem29  37709  poimirlem31  37711  poimirlem32  37712  sdclem2  37802  sdclem1  37803  prdsbnd2  37855  ismtyval  37860  rrnequiv  37895  isexid2  37915  ismndo1  37933  exidreslem  37937  rngo2  37967  rngoueqz  38000  risci  38047  prtlem11  38985  prtlem15  38994  cvrat4  39562  lcfl6  41619  dvdsexpnn0  42452  harval3  43655  clcnvlem  43740  cnvrcl0  43742  cnvtrcl0  43743  iunrelexpmin1  43825  iunrelexpmin2  43829  ormkglobd  46997  fcoresf1b  47194  aovmpt4g  47325  elsetpreimafvbi  47515  iccpartiltu  47546  iccpartgt  47551  iccpartgel  47553  reuopreuprim  47650  fmtnofac1  47694  gbepos  47882  grtrif1o  48066  grtriclwlk3  48069  isubgr3stgrlem4  48093  gpgprismgr4cycllem3  48221  pgnbgreunbgrlem1  48237  pgnbgreunbgrlem3  48242  pgnbgreunbgrlem4  48243  pgnbgreunbgrlem5lem1  48244  pgnbgreunbgrlem5lem2  48245  pgnbgreunbgrlem5lem3  48246  pgnbgreunbgrlem6  48248  pgnbgreunbgr  48249  ellcoellss  48560  dignn0flhalflem2  48741  nn0sumshdiglemB  48745  1arympt1  48763  opth1neg  48950  opth2neg  48951  oppccatb  49141  fullthinc  49575