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  2455  pm2.61ne  3033  spcimgft  3558  unineq  4307  elpreqprlem  4890  oteqex  5519  elopabrOLD  5582  otel3xp  5746  eqrelrdv2  5819  breldmg  5934  elrnmpt1  5983  cnveqb  6227  cnveq0  6228  predpoirr  6365  predfrirr  6366  limelon  6459  f1ssf1  6894  ndmfv  6955  eqfnun  7070  ffvresb  7159  isomin  7373  isofrlem  7376  oprabidw  7479  caovord3d  7660  eldifpw  7803  ssonuni  7815  onsucuni2  7870  ordzsl  7882  tfindsg  7898  findsg  7937  oteqimp  8049  frxp  8167  poxp  8169  fnwelem  8172  wfrlem14OLD  8378  tfrlem11  8444  ord1eln01  8552  ord2eln012  8553  oacl  8591  omcl  8592  oecl  8593  oa0r  8594  om0r  8595  om1r  8599  oe1m  8601  oaordi  8602  oawordri  8606  oaass  8617  oarec  8618  omwordri  8628  odi  8635  omass  8636  oewordri  8648  oeworde  8649  oeordsuc  8650  oelim2  8651  oeoa  8653  oeoelem  8654  oeoe  8655  nnm0r  8666  nnacl  8667  nnacom  8673  nnaordi  8674  nnaass  8678  nndi  8679  nnmass  8680  nnmsucr  8681  nnmcom  8682  omabs  8707  brecop  8868  eceqoveq  8880  elpm2r  8903  map0g  8942  undifixp  8992  fundmen  9096  mapxpen  9209  mapunen  9212  pssnn  9234  php  9273  phpOLD  9285  unxpdomlem2  9314  f1vrnfibi  9410  elfir  9484  wemapso2lem  9621  wdompwdom  9647  inf3lem1  9697  inf3lem3  9699  cantnfval2  9738  cantnfp1lem3  9749  r1sdom  9843  r1tr  9845  carden2a  10035  fidomtri2  10063  prdom2  10075  infxpenlem  10082  acndom  10120  fodomacn  10125  wdomfil  10130  alephon  10138  alephordi  10143  alephle  10157  alephfplem3  10175  dfac2a  10199  kmlem9  10228  cflm  10319  cfslb  10335  cfslbn  10336  infpssrlem3  10374  infpssrlem4  10375  fin23lem21  10408  fin23lem30  10411  isf34lem7  10448  isf34lem6  10449  fin67  10464  isfin7-2  10465  fin1a2lem7  10475  fin1a2lem10  10478  iundom2g  10609  konigthlem  10637  alephreg  10651  gchdomtri  10698  wunr1om  10788  tskr1om  10836  inar1  10844  grur1a  10888  indpi  10976  genpprecl  11070  genpnmax  11076  addcmpblnr  11138  recexsrlem  11172  map2psrpr  11179  ax1rid  11230  axpre-mulgt0  11237  ltle  11378  nnmulcl  12317  nnsub  12337  nn0sub  12603  nneo  12727  uz11  12928  xrltle  13211  xltnegi  13278  xrsupsslem  13369  xrinfmsslem  13370  xrub  13374  supxrunb1  13381  supxrunb2  13382  om2uzuzi  14000  uzrdgxfr  14018  seqcl2  14071  seqfveq2  14075  seqshft2  14079  seqsplit  14086  seqcaopr3  14088  seqf1olem2a  14091  seqid2  14099  seqhomo  14100  ser1const  14109  m1expcl2  14136  expadd  14155  expmul  14158  faclbnd  14339  hashfzp1  14480  hashmap  14484  hashf1lem2  14505  hashf1  14506  seqcoll  14513  wrdsymb0  14597  len0nnbi  14599  eqs1  14660  swrdnd2  14703  wrd2ind  14771  pfxccatin12lem2c  14778  pfxccatin12lem2  14779  swrdccatin1d  14791  repswccat  14834  repswcshw  14860  cshwcshid  14876  rtrclreclem3  15109  rtrclreclem4  15110  dfrtrcl2  15111  relexpindlem  15112  relexpind  15113  rtrclind  15114  recan  15385  rexanre  15395  rlimcn3  15636  caurcvg2  15726  fsumiun  15869  efexp  16149  rpnnen2lem12  16273  dvdstr  16342  alzdvds  16368  zob  16407  sumeven  16435  sumodd  16436  bitsinv1  16488  smu01lem  16531  smupval  16534  smueqlem  16536  smumullem  16538  seq1st  16618  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  cncongr2  16715  prmdiveq  16833  odzdvds  16842  pythagtriplem2  16864  pcexp  16906  vdwlem13  17040  ramz  17072  prmolefac  17093  elrestr  17488  xpsff1o  17627  subsubc  17917  clatl  18578  frmdgsum  18897  sursubmefmnd  18931  injsubmefmnd  18932  smndex1mndlem  18944  dfgrp3e  19080  mulgneg2  19148  mulgnnass  19149  mhmmulg  19155  gsumwrev  19409  symgextf1lem  19462  symgfixelsi  19477  pmtrdifellem4  19521  sylow1lem1  19640  efgsfo  19781  efgred  19790  cyggexb  19941  gsumzres  19951  gsum2dlem2  20013  mulgass2  20332  rngimcnv  20482  funcrngcsetc  20662  funcrngcsetcALT  20663  rhmsscrnghm  20687  funcringcsetc  20696  lmodprop2d  20944  lspsnne2  21143  lspsneu  21148  cnfldmulg  21439  cnfldexp  21440  zrhpsgnelbas  21635  assapropd  21915  mplcoe1  22078  mplcoe3  22079  mplcoe5  22081  mhpvarcl  22175  ply1sclf1  22313  mat1scmat  22566  restopn2  23206  cnpf2  23279  cmpfi  23437  txcn  23655  txlm  23677  xkoptsub  23683  xkopjcn  23685  ufildr  23960  cnflf  24031  fclsnei  24048  fclscmp  24059  ufilcmp  24061  cnfcf  24071  symgtgp  24135  isxms2  24479  met2ndc  24557  metustbl  24600  tngngp2  24694  clmmulg  25153  iscau4  25332  ovolunlem1a  25550  ovolicc2lem4  25574  volfiniun  25601  voliunlem1  25604  volsup  25610  dvnadd  25985  dvnres  25987  dvcobr  26003  dvcobrOLD  26004  ply1nzb  26182  plypf1  26271  dgrle  26302  coeaddlem  26308  dgrlt  26326  dvntaylp  26431  cxpmul2  26749  rlimcnp  27026  facgam  27127  wilthlem2  27130  isnsqf  27196  musum  27252  chtub  27274  chpval2  27280  gausslemma2dlem0i  27426  dchrisumlem1  27551  qabvexp  27688  ostthlem2  27690  nodenselem8  27754  slerec  27882  bday1s  27894  ssltleft  27927  ssltright  27928  noseqind  28316  dfnns2  28380  axsegconlem1  28950  ax5seglem4  28965  ax5seglem5  28966  axlowdimlem15  28989  axcontlem2  28998  axcontlem4  29000  incistruhgr  29114  upgredg2vtx  29176  upgredgpr  29177  numedglnl  29179  uhgr2edg  29243  nbupgruvtxres  29442  cusgrfilem1  29491  wlkres  29706  wlkp1lem2  29710  pthdivtx  29765  pthdlem2lem  29803  wlkiswwlks2lem4  29905  wwlksnredwwlkn0  29929  wwlksnextwrd  29930  wwlksnfi  29939  wwlksnextprop  29945  clwlkclwwlklem2a  30030  clwlkclwwlkf1lem2  30037  erclwwlksym  30053  clwwlkf1  30081  eleclclwwlknlem2  30093  erclwwlknsym  30102  clwwlknonex2  30141  eupth2lem3lem6  30265  frgr3vlem1  30305  3vfriswmgrlem  30309  wlkl0  30399  sspval  30755  nmosetre  30796  nmobndseqi  30811  nmobndseqiALT  30812  orthcom  31140  shsva  31352  shmodsi  31421  h1datomi  31613  nmopsetretALT  31895  nmfnsetre  31909  lnopcnbd  32068  pjclem4  32231  pj3si  32239  ssmd1  32343  atom1d  32385  chjatom  32389  atcvat4i  32429  cdj3lem2a  32468  cdj3lem3a  32471  disjunsn  32616  unitdivcld  33847  xrge0iifiso  33881  dya2iocuni  34248  bnj168  34706  bnj535  34866  bnj590  34886  bnj594  34888  bnj938  34913  bnj1118  34960  bnj1128  34966  fnrelpredd  35065  deranglem  35134  subfacp1lem6  35153  subfacval2  35155  cvmlift2lem12  35282  satffun  35377  mrsubvrs  35490  msrrcl  35511  mclsax  35537  dfon2lem6  35752  rdgprc  35758  ifscgr  36008  btwncolinear1  36033  hfelhf  36145  opnrebl2  36287  nn0prpw  36289  ordcmp  36413  findreccl  36419  nndivlub  36424  bj-rest0  37059  bj-isrvec2  37266  topdifinffinlem  37313  iooelexlt  37328  rdgeqoa  37336  exrecfnlem  37345  wl-mo3t  37530  matunitlindflem2  37577  poimirlem2  37582  poimirlem23  37603  poimirlem28  37608  poimirlem29  37609  poimirlem31  37611  poimirlem32  37612  sdclem2  37702  sdclem1  37703  prdsbnd2  37755  ismtyval  37760  rrnequiv  37795  isexid2  37815  ismndo1  37833  exidreslem  37837  rngo2  37867  rngoueqz  37900  risci  37947  prtlem11  38822  prtlem15  38831  cvrat4  39400  lcfl6  41457  dvdsexpnn0  42321  harval3  43500  clcnvlem  43585  cnvrcl0  43587  cnvtrcl0  43588  iunrelexpmin1  43670  iunrelexpmin2  43674  tworepnotupword  46805  fcoresf1b  46985  aovmpt4g  47116  elsetpreimafvbi  47265  iccpartiltu  47296  iccpartgt  47301  iccpartgel  47303  reuopreuprim  47400  fmtnofac1  47444  gbepos  47632  grtrif1o  47793  grtriclwlk3  47796  ellcoellss  48164  dignn0flhalflem2  48350  nn0sumshdiglemB  48354  1arympt1  48372  fullthinc  48713