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  2445  pm2.61ne  3010  spcimgft  3512  unineq  4251  elpreqprlem  4830  oteqex  5460  elopabrOLD  5523  otel3xp  5684  eqrelrdv2  5758  breldmg  5873  elrnmpt1  5924  cnveqb  6169  cnveq0  6170  predpoirr  6306  predfrirr  6307  limelon  6397  f1ssf1  6832  ndmfv  6893  eqfnun  7009  ffvresb  7097  isomin  7312  isofrlem  7315  oprabidw  7418  caovord3d  7599  eldifpw  7744  ssonuni  7756  onsucuni2  7809  ordzsl  7821  tfindsg  7837  findsg  7873  oteqimp  7987  frxp  8105  poxp  8107  fnwelem  8110  tfrlem11  8356  ord1eln01  8460  ord2eln012  8461  oacl  8499  omcl  8500  oecl  8501  oa0r  8502  om0r  8503  om1r  8507  oe1m  8509  oaordi  8510  oawordri  8514  oaass  8525  oarec  8526  omwordri  8536  odi  8543  omass  8544  oewordri  8556  oeworde  8557  oeordsuc  8558  oelim2  8559  oeoa  8561  oeoelem  8562  oeoe  8563  nnm0r  8574  nnacl  8575  nnacom  8581  nnaordi  8582  nnaass  8586  nndi  8587  nnmass  8588  nnmsucr  8589  nnmcom  8590  omabs  8615  brecop  8783  eceqoveq  8795  elpm2r  8818  map0g  8857  undifixp  8907  fundmen  9002  mapxpen  9107  mapunen  9110  pssnn  9132  php  9171  unxpdomlem2  9198  f1vrnfibi  9293  elfir  9366  wemapso2lem  9505  wdompwdom  9531  inf3lem1  9581  inf3lem3  9583  cantnfval2  9622  cantnfp1lem3  9633  r1sdom  9727  r1tr  9729  carden2a  9919  fidomtri2  9947  prdom2  9959  infxpenlem  9966  acndom  10004  fodomacn  10009  wdomfil  10014  alephon  10022  alephordi  10027  alephle  10041  alephfplem3  10059  dfac2a  10083  kmlem9  10112  cflm  10203  cfslb  10219  cfslbn  10220  infpssrlem3  10258  infpssrlem4  10259  fin23lem21  10292  fin23lem30  10295  isf34lem7  10332  isf34lem6  10333  fin67  10348  isfin7-2  10349  fin1a2lem7  10359  fin1a2lem10  10362  iundom2g  10493  konigthlem  10521  alephreg  10535  gchdomtri  10582  wunr1om  10672  tskr1om  10720  inar1  10728  grur1a  10772  indpi  10860  genpprecl  10954  genpnmax  10960  addcmpblnr  11022  recexsrlem  11056  map2psrpr  11063  ax1rid  11114  axpre-mulgt0  11121  ltle  11262  nnmulcl  12210  nnsub  12230  nn0sub  12492  nneo  12618  uz11  12818  xrltle  13109  xltnegi  13176  xrsupsslem  13267  xrinfmsslem  13268  xrub  13272  supxrunb1  13279  supxrunb2  13280  om2uzuzi  13914  uzrdgxfr  13932  seqcl2  13985  seqfveq2  13989  seqshft2  13993  seqsplit  14000  seqcaopr3  14002  seqf1olem2a  14005  seqid2  14013  seqhomo  14014  ser1const  14023  m1expcl2  14050  expadd  14069  expmul  14072  faclbnd  14255  hashfzp1  14396  hashmap  14400  hashf1lem2  14421  hashf1  14422  seqcoll  14429  wrdsymb0  14514  len0nnbi  14516  eqs1  14577  swrdnd2  14620  wrd2ind  14688  pfxccatin12lem2c  14695  pfxccatin12lem2  14696  swrdccatin1d  14708  repswccat  14751  repswcshw  14777  cshwcshid  14793  rtrclreclem3  15026  rtrclreclem4  15027  dfrtrcl2  15028  relexpindlem  15029  relexpind  15030  rtrclind  15031  recan  15303  rexanre  15313  rlimcn3  15556  caurcvg2  15644  fsumiun  15787  efexp  16069  rpnnen2lem12  16193  dvdstr  16264  alzdvds  16290  zob  16329  sumeven  16357  sumodd  16358  bitsinv1  16412  smu01lem  16455  smupval  16458  smueqlem  16460  smumullem  16462  seq1st  16541  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  cncongr2  16638  prmdiveq  16756  odzdvds  16766  pythagtriplem2  16788  pcexp  16830  vdwlem13  16964  ramz  16996  prmolefac  17017  elrestr  17391  xpsff1o  17530  subsubc  17815  clatl  18467  frmdgsum  18789  sursubmefmnd  18823  injsubmefmnd  18824  smndex1mndlem  18836  dfgrp3e  18972  mulgneg2  19040  mulgnnass  19041  mhmmulg  19047  gsumwrev  19298  symgextf1lem  19350  symgfixelsi  19365  pmtrdifellem4  19409  sylow1lem1  19528  efgsfo  19669  efgred  19678  cyggexb  19829  gsumzres  19839  gsum2dlem2  19901  mulgass2  20218  rngimcnv  20365  funcrngcsetc  20549  funcrngcsetcALT  20550  rhmsscrnghm  20574  funcringcsetc  20583  lmodprop2d  20830  lspsnne2  21028  lspsneu  21033  cnfldmulg  21315  cnfldexp  21316  zrhpsgnelbas  21503  assapropd  21781  mplcoe1  21944  mplcoe3  21945  mplcoe5  21947  mhpvarcl  22035  ply1sclf1  22175  mat1scmat  22426  restopn2  23064  cnpf2  23137  cmpfi  23295  txcn  23513  txlm  23535  xkoptsub  23541  xkopjcn  23543  ufildr  23818  cnflf  23889  fclsnei  23906  fclscmp  23917  ufilcmp  23919  cnfcf  23929  symgtgp  23993  isxms2  24336  met2ndc  24411  metustbl  24454  tngngp2  24540  clmmulg  25001  iscau4  25179  ovolunlem1a  25397  ovolicc2lem4  25421  volfiniun  25448  voliunlem1  25451  volsup  25457  dvnadd  25831  dvnres  25833  dvcobr  25849  dvcobrOLD  25850  ply1nzb  26028  plypf1  26117  dgrle  26148  coeaddlem  26154  dgrlt  26172  dvntaylp  26279  cxpmul2  26598  rlimcnp  26875  facgam  26976  wilthlem2  26979  isnsqf  27045  musum  27101  chtub  27123  chpval2  27129  gausslemma2dlem0i  27275  dchrisumlem1  27400  qabvexp  27537  ostthlem2  27539  nodenselem8  27603  slerec  27731  bday1s  27743  ssltleft  27782  ssltright  27783  onscutlt  28165  noseqind  28186  dfnns2  28261  axsegconlem1  28844  ax5seglem4  28859  ax5seglem5  28860  axlowdimlem15  28883  axcontlem2  28892  axcontlem4  28894  incistruhgr  29006  upgredg2vtx  29068  upgredgpr  29069  numedglnl  29071  uhgr2edg  29135  nbupgruvtxres  29334  cusgrfilem1  29383  wlkres  29598  wlkp1lem2  29602  pthdivtx  29657  pthdlem2lem  29697  wlkiswwlks2lem4  29802  wwlksnredwwlkn0  29826  wwlksnextwrd  29827  wwlksnfi  29836  wwlksnextprop  29842  clwlkclwwlklem2a  29927  clwlkclwwlkf1lem2  29934  erclwwlksym  29950  clwwlkf1  29978  eleclclwwlknlem2  29990  erclwwlknsym  29999  clwwlknonex2  30038  eupth2lem3lem6  30162  frgr3vlem1  30202  3vfriswmgrlem  30206  wlkl0  30296  sspval  30652  nmosetre  30693  nmobndseqi  30708  nmobndseqiALT  30709  orthcom  31037  shsva  31249  shmodsi  31318  h1datomi  31510  nmopsetretALT  31792  nmfnsetre  31806  lnopcnbd  31965  pjclem4  32128  pj3si  32136  ssmd1  32240  atom1d  32282  chjatom  32286  atcvat4i  32326  cdj3lem2a  32365  cdj3lem3a  32368  disjunsn  32523  unitdivcld  33891  xrge0iifiso  33925  dya2iocuni  34274  bnj168  34720  bnj535  34880  bnj590  34900  bnj594  34902  bnj938  34927  bnj1118  34974  bnj1128  34980  fnrelpredd  35079  deranglem  35153  subfacp1lem6  35172  subfacval2  35174  cvmlift2lem12  35301  satffun  35396  mrsubvrs  35509  msrrcl  35530  mclsax  35556  dfon2lem6  35776  rdgprc  35782  ifscgr  36032  btwncolinear1  36057  hfelhf  36169  opnrebl2  36309  nn0prpw  36311  ordcmp  36435  findreccl  36441  nndivlub  36446  bj-rest0  37081  bj-isrvec2  37288  topdifinffinlem  37335  iooelexlt  37350  rdgeqoa  37358  exrecfnlem  37367  wl-mo3t  37564  matunitlindflem2  37611  poimirlem2  37616  poimirlem23  37637  poimirlem28  37642  poimirlem29  37643  poimirlem31  37645  poimirlem32  37646  sdclem2  37736  sdclem1  37737  prdsbnd2  37789  ismtyval  37794  rrnequiv  37829  isexid2  37849  ismndo1  37867  exidreslem  37871  rngo2  37901  rngoueqz  37934  risci  37981  prtlem11  38859  prtlem15  38868  cvrat4  39437  lcfl6  41494  dvdsexpnn0  42322  harval3  43527  clcnvlem  43612  cnvrcl0  43614  cnvtrcl0  43615  iunrelexpmin1  43697  iunrelexpmin2  43701  ormkglobd  46873  tworepnotupword  46884  fcoresf1b  47071  aovmpt4g  47202  elsetpreimafvbi  47392  iccpartiltu  47423  iccpartgt  47428  iccpartgel  47430  reuopreuprim  47527  fmtnofac1  47571  gbepos  47759  grtrif1o  47941  grtriclwlk3  47944  isubgr3stgrlem4  47968  gpgprismgr4cycllem3  48087  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5lem3  48112  pgnbgreunbgrlem6  48114  pgnbgreunbgr  48115  ellcoellss  48424  dignn0flhalflem2  48605  nn0sumshdiglemB  48609  1arympt1  48627  opth1neg  48814  opth2neg  48815  oppccatb  49005  fullthinc  49439