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  2451  pm2.61ne  3017  spcimgft  3491  unineq  4228  elpreqprlem  4809  oteqex  5454  otel3xp  5677  eqrelrdv2  5751  breldmg  5864  elrnmpt1  5915  cnveqb  6160  cnveq0  6161  predpoirr  6297  predfrirr  6298  limelon  6388  f1ssf1  6812  ndmfv  6872  eqfnun  6989  ffvresb  7078  isomin  7292  isofrlem  7295  oprabidw  7398  caovord3d  7577  eldifpw  7722  ssonuni  7734  onsucuni2  7785  ordzsl  7796  tfindsg  7812  findsg  7848  oteqimp  7961  frxp  8076  poxp  8078  fnwelem  8081  tfrlem11  8327  ord1eln01  8431  ord2eln012  8432  oacl  8470  omcl  8471  oecl  8472  oa0r  8473  om0r  8474  om1r  8478  oe1m  8480  oaordi  8481  oawordri  8485  oaass  8496  oarec  8497  omwordri  8507  odi  8514  omass  8515  oewordri  8528  oeworde  8529  oeordsuc  8530  oelim2  8531  oeoa  8533  oeoelem  8534  oeoe  8535  nnm0r  8546  nnacl  8547  nnacom  8553  nnaordi  8554  nnaass  8558  nndi  8559  nnmass  8560  nnmsucr  8561  nnmcom  8562  omabs  8587  brecop  8757  eceqoveq  8769  elpm2r  8792  map0g  8832  undifixp  8882  fundmen  8978  mapxpen  9081  mapunen  9084  pssnn  9103  php  9141  unxpdomlem2  9167  f1vrnfibi  9252  elfir  9328  wemapso2lem  9467  wdompwdom  9493  inf3lem1  9549  inf3lem3  9551  cantnfval2  9590  cantnfp1lem3  9601  r1sdom  9698  r1tr  9700  carden2a  9890  fidomtri2  9918  prdom2  9928  infxpenlem  9935  acndom  9973  fodomacn  9978  wdomfil  9983  alephon  9991  alephordi  9996  alephle  10010  alephfplem3  10028  dfac2a  10052  kmlem9  10081  cflm  10172  cfslb  10188  cfslbn  10189  infpssrlem3  10227  infpssrlem4  10228  fin23lem21  10261  fin23lem30  10264  isf34lem7  10301  isf34lem6  10302  fin67  10317  isfin7-2  10318  fin1a2lem7  10328  fin1a2lem10  10331  iundom2g  10462  konigthlem  10491  alephreg  10505  gchdomtri  10552  wunr1om  10642  tskr1om  10690  inar1  10698  grur1a  10742  indpi  10830  genpprecl  10924  genpnmax  10930  addcmpblnr  10992  recexsrlem  11026  map2psrpr  11033  ax1rid  11084  axpre-mulgt0  11091  ltle  11234  nnmulcl  12198  nnsub  12221  nn0sub  12487  nneo  12613  uz11  12813  xrltle  13100  xltnegi  13168  xrsupsslem  13259  xrinfmsslem  13260  xrub  13264  supxrunb1  13271  supxrunb2  13272  om2uzuzi  13911  uzrdgxfr  13929  seqcl2  13982  seqfveq2  13986  seqshft2  13990  seqsplit  13997  seqcaopr3  13999  seqf1olem2a  14002  seqid2  14010  seqhomo  14011  ser1const  14020  m1expcl2  14047  expadd  14066  expmul  14069  faclbnd  14252  hashfzp1  14393  hashmap  14397  hashf1lem2  14418  hashf1  14419  seqcoll  14426  wrdsymb0  14511  len0nnbi  14513  eqs1  14575  swrdnd2  14618  wrd2ind  14685  pfxccatin12lem2c  14692  pfxccatin12lem2  14693  swrdccatin1d  14705  repswccat  14748  repswcshw  14774  cshwcshid  14789  rtrclreclem3  15022  rtrclreclem4  15023  dfrtrcl2  15024  relexpindlem  15025  relexpind  15026  rtrclind  15027  recan  15299  rexanre  15309  rlimcn3  15552  caurcvg2  15640  fsumiun  15784  efexp  16068  rpnnen2lem12  16192  dvdstr  16263  alzdvds  16289  zob  16328  sumeven  16356  sumodd  16357  bitsinv1  16411  smu01lem  16454  smupval  16457  smueqlem  16459  smumullem  16461  seq1st  16540  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  cncongr2  16637  prmdiveq  16756  odzdvds  16766  pythagtriplem2  16788  pcexp  16830  vdwlem13  16964  ramz  16996  prmolefac  17017  elrestr  17391  xpsff1o  17531  subsubc  17820  clatl  18474  frmdgsum  18830  sursubmefmnd  18864  injsubmefmnd  18865  smndex1mndlem  18880  dfgrp3e  19016  mulgneg2  19084  mulgnnass  19085  mhmmulg  19091  gsumwrev  19341  symgextf1lem  19395  symgfixelsi  19410  pmtrdifellem4  19454  sylow1lem1  19573  efgsfo  19714  efgred  19723  cyggexb  19874  gsumzres  19884  gsum2dlem2  19946  mulgass2  20290  rngimcnv  20436  funcrngcsetc  20617  funcrngcsetcALT  20618  rhmsscrnghm  20642  funcringcsetc  20651  lmodprop2d  20919  lspsnne2  21116  lspsneu  21121  cnfldmulg  21384  cnfldexp  21385  zrhpsgnelbas  21574  assapropd  21851  mplcoe1  22015  mplcoe3  22016  mplcoe5  22018  mhpvarcl  22114  ply1sclf1  22254  mat1scmat  22504  restopn2  23142  cnpf2  23215  cmpfi  23373  txcn  23591  txlm  23613  xkoptsub  23619  xkopjcn  23621  ufildr  23896  cnflf  23967  fclsnei  23984  fclscmp  23995  ufilcmp  23997  cnfcf  24007  symgtgp  24071  isxms2  24413  met2ndc  24488  metustbl  24531  tngngp2  24617  clmmulg  25068  iscau4  25246  ovolunlem1a  25463  ovolicc2lem4  25487  volfiniun  25514  voliunlem1  25517  volsup  25523  dvnadd  25896  dvnres  25898  dvcobr  25913  ply1nzb  26088  plypf1  26177  dgrle  26208  coeaddlem  26214  dgrlt  26231  dvntaylp  26336  cxpmul2  26653  rlimcnp  26929  facgam  27029  wilthlem2  27032  isnsqf  27098  musum  27154  chtub  27175  chpval2  27181  gausslemma2dlem0i  27327  dchrisumlem1  27452  qabvexp  27589  ostthlem2  27591  nodenselem8  27655  lesrec  27791  bday1  27806  sltsleft  27852  sltsright  27853  oncutlt  28256  noseqind  28284  dfnns2  28364  bdaypw2n0bnd  28456  axsegconlem1  28986  ax5seglem4  29001  ax5seglem5  29002  axlowdimlem15  29025  axcontlem2  29034  axcontlem4  29036  incistruhgr  29148  upgredg2vtx  29210  upgredgpr  29211  numedglnl  29213  uhgr2edg  29277  nbupgruvtxres  29476  cusgrfilem1  29524  wlkres  29737  wlkp1lem2  29741  pthdivtx  29795  pthdlem2lem  29835  wlkiswwlks2lem4  29940  wwlksnredwwlkn0  29964  wwlksnextwrd  29965  wwlksnfi  29974  wwlksnextprop  29980  clwlkclwwlklem2a  30068  clwlkclwwlkf1lem2  30075  erclwwlksym  30091  clwwlkf1  30119  eleclclwwlknlem2  30131  erclwwlknsym  30140  clwwlknonex2  30179  eupth2lem3lem6  30303  frgr3vlem1  30343  3vfriswmgrlem  30347  wlkl0  30437  sspval  30794  nmosetre  30835  nmobndseqi  30850  nmobndseqiALT  30851  orthcom  31179  shsva  31391  shmodsi  31460  h1datomi  31652  nmopsetretALT  31934  nmfnsetre  31948  lnopcnbd  32107  pjclem4  32270  pj3si  32278  ssmd1  32382  atom1d  32424  chjatom  32428  atcvat4i  32468  cdj3lem2a  32507  cdj3lem3a  32510  disjunsn  32664  unitdivcld  34045  xrge0iifiso  34079  dya2iocuni  34427  bnj168  34873  bnj535  35032  bnj590  35052  bnj594  35054  bnj938  35079  bnj1118  35126  bnj1128  35132  fnrelpredd  35234  deranglem  35348  subfacp1lem6  35367  subfacval2  35369  cvmlift2lem12  35496  satffun  35591  mrsubvrs  35704  msrrcl  35725  mclsax  35751  dfon2lem6  35968  rdgprc  35974  ifscgr  36226  btwncolinear1  36251  hfelhf  36363  opnrebl2  36503  nn0prpw  36505  ordcmp  36629  findreccl  36635  nndivlub  36640  axtcond  36660  dfttc2g  36688  mh-inf3f1  36723  bj-rest0  37405  bj-isrvec2  37614  topdifinffinlem  37663  iooelexlt  37678  rdgeqoa  37686  exrecfnlem  37695  wl-mo3t  37901  matunitlindflem2  37938  poimirlem2  37943  poimirlem23  37964  poimirlem28  37969  poimirlem29  37970  poimirlem31  37972  poimirlem32  37973  sdclem2  38063  sdclem1  38064  prdsbnd2  38116  ismtyval  38121  rrnequiv  38156  isexid2  38176  ismndo1  38194  exidreslem  38198  rngo2  38228  rngoueqz  38261  risci  38308  eldisjdmqsim  39138  prtlem11  39312  prtlem15  39321  cvrat4  39889  lcfl6  41946  dvdsexpnn0  42766  harval3  43965  clcnvlem  44050  cnvrcl0  44052  cnvtrcl0  44053  iunrelexpmin1  44135  iunrelexpmin2  44139  ormkglobd  47305  fcoresf1b  47518  aovmpt4g  47649  elsetpreimafvbi  47851  iccpartiltu  47882  iccpartgt  47887  iccpartgel  47889  reuopreuprim  47986  fmtnofac1  48033  gbepos  48234  grtrif1o  48418  grtriclwlk3  48421  isubgr3stgrlem4  48445  gpgprismgr4cycllem3  48573  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5lem3  48598  pgnbgreunbgrlem6  48600  pgnbgreunbgr  48601  ellcoellss  48911  dignn0flhalflem2  49092  nn0sumshdiglemB  49096  1arympt1  49114  opth1neg  49301  opth2neg  49302  oppccatb  49491  fullthinc  49925