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  2446  pm2.61ne  3011  spcimgft  3515  unineq  4254  elpreqprlem  4833  oteqex  5463  elopabrOLD  5526  otel3xp  5687  eqrelrdv2  5761  breldmg  5876  elrnmpt1  5927  cnveqb  6172  cnveq0  6173  predpoirr  6309  predfrirr  6310  limelon  6400  f1ssf1  6835  ndmfv  6896  eqfnun  7012  ffvresb  7100  isomin  7315  isofrlem  7318  oprabidw  7421  caovord3d  7602  eldifpw  7747  ssonuni  7759  onsucuni2  7812  ordzsl  7824  tfindsg  7840  findsg  7876  oteqimp  7990  frxp  8108  poxp  8110  fnwelem  8113  tfrlem11  8359  ord1eln01  8463  ord2eln012  8464  oacl  8502  omcl  8503  oecl  8504  oa0r  8505  om0r  8506  om1r  8510  oe1m  8512  oaordi  8513  oawordri  8517  oaass  8528  oarec  8529  omwordri  8539  odi  8546  omass  8547  oewordri  8559  oeworde  8560  oeordsuc  8561  oelim2  8562  oeoa  8564  oeoelem  8565  oeoe  8566  nnm0r  8577  nnacl  8578  nnacom  8584  nnaordi  8585  nnaass  8589  nndi  8590  nnmass  8591  nnmsucr  8592  nnmcom  8593  omabs  8618  brecop  8786  eceqoveq  8798  elpm2r  8821  map0g  8860  undifixp  8910  fundmen  9005  mapxpen  9113  mapunen  9116  pssnn  9138  php  9177  unxpdomlem2  9205  f1vrnfibi  9300  elfir  9373  wemapso2lem  9512  wdompwdom  9538  inf3lem1  9588  inf3lem3  9590  cantnfval2  9629  cantnfp1lem3  9640  r1sdom  9734  r1tr  9736  carden2a  9926  fidomtri2  9954  prdom2  9966  infxpenlem  9973  acndom  10011  fodomacn  10016  wdomfil  10021  alephon  10029  alephordi  10034  alephle  10048  alephfplem3  10066  dfac2a  10090  kmlem9  10119  cflm  10210  cfslb  10226  cfslbn  10227  infpssrlem3  10265  infpssrlem4  10266  fin23lem21  10299  fin23lem30  10302  isf34lem7  10339  isf34lem6  10340  fin67  10355  isfin7-2  10356  fin1a2lem7  10366  fin1a2lem10  10369  iundom2g  10500  konigthlem  10528  alephreg  10542  gchdomtri  10589  wunr1om  10679  tskr1om  10727  inar1  10735  grur1a  10779  indpi  10867  genpprecl  10961  genpnmax  10967  addcmpblnr  11029  recexsrlem  11063  map2psrpr  11070  ax1rid  11121  axpre-mulgt0  11128  ltle  11269  nnmulcl  12217  nnsub  12237  nn0sub  12499  nneo  12625  uz11  12825  xrltle  13116  xltnegi  13183  xrsupsslem  13274  xrinfmsslem  13275  xrub  13279  supxrunb1  13286  supxrunb2  13287  om2uzuzi  13921  uzrdgxfr  13939  seqcl2  13992  seqfveq2  13996  seqshft2  14000  seqsplit  14007  seqcaopr3  14009  seqf1olem2a  14012  seqid2  14020  seqhomo  14021  ser1const  14030  m1expcl2  14057  expadd  14076  expmul  14079  faclbnd  14262  hashfzp1  14403  hashmap  14407  hashf1lem2  14428  hashf1  14429  seqcoll  14436  wrdsymb0  14521  len0nnbi  14523  eqs1  14584  swrdnd2  14627  wrd2ind  14695  pfxccatin12lem2c  14702  pfxccatin12lem2  14703  swrdccatin1d  14715  repswccat  14758  repswcshw  14784  cshwcshid  14800  rtrclreclem3  15033  rtrclreclem4  15034  dfrtrcl2  15035  relexpindlem  15036  relexpind  15037  rtrclind  15038  recan  15310  rexanre  15320  rlimcn3  15563  caurcvg2  15651  fsumiun  15794  efexp  16076  rpnnen2lem12  16200  dvdstr  16271  alzdvds  16297  zob  16336  sumeven  16364  sumodd  16365  bitsinv1  16419  smu01lem  16462  smupval  16465  smueqlem  16467  smumullem  16469  seq1st  16548  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  cncongr2  16645  prmdiveq  16763  odzdvds  16773  pythagtriplem2  16795  pcexp  16837  vdwlem13  16971  ramz  17003  prmolefac  17024  elrestr  17398  xpsff1o  17537  subsubc  17822  clatl  18474  frmdgsum  18796  sursubmefmnd  18830  injsubmefmnd  18831  smndex1mndlem  18843  dfgrp3e  18979  mulgneg2  19047  mulgnnass  19048  mhmmulg  19054  gsumwrev  19305  symgextf1lem  19357  symgfixelsi  19372  pmtrdifellem4  19416  sylow1lem1  19535  efgsfo  19676  efgred  19685  cyggexb  19836  gsumzres  19846  gsum2dlem2  19908  mulgass2  20225  rngimcnv  20372  funcrngcsetc  20556  funcrngcsetcALT  20557  rhmsscrnghm  20581  funcringcsetc  20590  lmodprop2d  20837  lspsnne2  21035  lspsneu  21040  cnfldmulg  21322  cnfldexp  21323  zrhpsgnelbas  21510  assapropd  21788  mplcoe1  21951  mplcoe3  21952  mplcoe5  21954  mhpvarcl  22042  ply1sclf1  22182  mat1scmat  22433  restopn2  23071  cnpf2  23144  cmpfi  23302  txcn  23520  txlm  23542  xkoptsub  23548  xkopjcn  23550  ufildr  23825  cnflf  23896  fclsnei  23913  fclscmp  23924  ufilcmp  23926  cnfcf  23936  symgtgp  24000  isxms2  24343  met2ndc  24418  metustbl  24461  tngngp2  24547  clmmulg  25008  iscau4  25186  ovolunlem1a  25404  ovolicc2lem4  25428  volfiniun  25455  voliunlem1  25458  volsup  25464  dvnadd  25838  dvnres  25840  dvcobr  25856  dvcobrOLD  25857  ply1nzb  26035  plypf1  26124  dgrle  26155  coeaddlem  26161  dgrlt  26179  dvntaylp  26286  cxpmul2  26605  rlimcnp  26882  facgam  26983  wilthlem2  26986  isnsqf  27052  musum  27108  chtub  27130  chpval2  27136  gausslemma2dlem0i  27282  dchrisumlem1  27407  qabvexp  27544  ostthlem2  27546  nodenselem8  27610  slerec  27738  bday1s  27750  ssltleft  27789  ssltright  27790  onscutlt  28172  noseqind  28193  dfnns2  28268  axsegconlem1  28851  ax5seglem4  28866  ax5seglem5  28867  axlowdimlem15  28890  axcontlem2  28899  axcontlem4  28901  incistruhgr  29013  upgredg2vtx  29075  upgredgpr  29076  numedglnl  29078  uhgr2edg  29142  nbupgruvtxres  29341  cusgrfilem1  29390  wlkres  29605  wlkp1lem2  29609  pthdivtx  29664  pthdlem2lem  29704  wlkiswwlks2lem4  29809  wwlksnredwwlkn0  29833  wwlksnextwrd  29834  wwlksnfi  29843  wwlksnextprop  29849  clwlkclwwlklem2a  29934  clwlkclwwlkf1lem2  29941  erclwwlksym  29957  clwwlkf1  29985  eleclclwwlknlem2  29997  erclwwlknsym  30006  clwwlknonex2  30045  eupth2lem3lem6  30169  frgr3vlem1  30209  3vfriswmgrlem  30213  wlkl0  30303  sspval  30659  nmosetre  30700  nmobndseqi  30715  nmobndseqiALT  30716  orthcom  31044  shsva  31256  shmodsi  31325  h1datomi  31517  nmopsetretALT  31799  nmfnsetre  31813  lnopcnbd  31972  pjclem4  32135  pj3si  32143  ssmd1  32247  atom1d  32289  chjatom  32293  atcvat4i  32333  cdj3lem2a  32372  cdj3lem3a  32375  disjunsn  32530  unitdivcld  33898  xrge0iifiso  33932  dya2iocuni  34281  bnj168  34727  bnj535  34887  bnj590  34907  bnj594  34909  bnj938  34934  bnj1118  34981  bnj1128  34987  fnrelpredd  35086  deranglem  35160  subfacp1lem6  35179  subfacval2  35181  cvmlift2lem12  35308  satffun  35403  mrsubvrs  35516  msrrcl  35537  mclsax  35563  dfon2lem6  35783  rdgprc  35789  ifscgr  36039  btwncolinear1  36064  hfelhf  36176  opnrebl2  36316  nn0prpw  36318  ordcmp  36442  findreccl  36448  nndivlub  36453  bj-rest0  37088  bj-isrvec2  37295  topdifinffinlem  37342  iooelexlt  37357  rdgeqoa  37365  exrecfnlem  37374  wl-mo3t  37571  matunitlindflem2  37618  poimirlem2  37623  poimirlem23  37644  poimirlem28  37649  poimirlem29  37650  poimirlem31  37652  poimirlem32  37653  sdclem2  37743  sdclem1  37744  prdsbnd2  37796  ismtyval  37801  rrnequiv  37836  isexid2  37856  ismndo1  37874  exidreslem  37878  rngo2  37908  rngoueqz  37941  risci  37988  prtlem11  38866  prtlem15  38875  cvrat4  39444  lcfl6  41501  dvdsexpnn0  42329  harval3  43534  clcnvlem  43619  cnvrcl0  43621  cnvtrcl0  43622  iunrelexpmin1  43704  iunrelexpmin2  43708  ormkglobd  46880  tworepnotupword  46891  fcoresf1b  47075  aovmpt4g  47206  elsetpreimafvbi  47396  iccpartiltu  47427  iccpartgt  47432  iccpartgel  47434  reuopreuprim  47531  fmtnofac1  47575  gbepos  47763  grtrif1o  47945  grtriclwlk3  47948  isubgr3stgrlem4  47972  gpgprismgr4cycllem3  48091  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  pgnbgreunbgrlem5lem3  48116  pgnbgreunbgrlem6  48118  pgnbgreunbgr  48119  ellcoellss  48428  dignn0flhalflem2  48609  nn0sumshdiglemB  48613  1arympt1  48631  opth1neg  48818  opth2neg  48819  oppccatb  49009  fullthinc  49443