Theorem imbitrrid 248

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 225	. 2 ⊢ (𝜒 → (𝜃 ↔ 𝜓))
4	1, 3	imbitrid 246	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  syl5ibrcom  249  biimprd  250  exdistrf  2477  pm2.61ne  3041  spcimgft  3513  unineq  4238  elpreqprlem  4821  oteqex  5466  otel3xp  5689  eqrelrdv2  5763  breldmg  5881  elrnmpt1  5932  cnveqb  6177  cnveq0  6178  predpoirr  6314  predfrirr  6315  limelon  6405  f1ssf1  6833  ndmfv  6893  eqfnun  7012  ffvresb  7101  isomin  7315  isofrlem  7318  oprabidw  7421  caovord3d  7600  eldifpw  7745  ssonuni  7757  onsucuni2  7808  ordzsl  7819  tfindsg  7835  findsg  7872  oteqimp  7983  frxp  8099  poxp  8101  fnwelem  8104  tfrlem11  8352  ord1eln01  8458  ord2eln012  8459  oacl  8497  omcl  8498  oecl  8499  oa0r  8500  om0r  8501  om1r  8505  oe1m  8507  oaordi  8508  oawordri  8512  oaass  8523  oarec  8524  omwordri  8534  odi  8541  omass  8542  oewordri  8555  oeworde  8556  oeordsuc  8557  oelim2  8558  oeoa  8560  oeoelem  8561  oeoe  8562  nnm0r  8573  nnacl  8574  nnacom  8580  nnaordi  8581  nnaass  8585  nndi  8586  nnmass  8587  nnmsucr  8588  nnmcom  8589  omabs  8614  brecop  8785  eceqoveq  8797  elpm2r  8819  map0g  8859  undifixp  8909  fundmen  9005  mapxpen  9108  mapunen  9111  pssnn  9130  php  9168  unxpdomlem2  9194  f1vrnfibi  9278  elfir  9354  wemapso2lem  9493  wdompwdom  9519  inf3lem1  9576  inf3lem3  9578  cantnfval2  9617  cantnfp1lem3  9628  r1sdom  9725  r1tr  9727  carden2a  9917  fidomtri2  9945  prdom2  9955  infxpenlem  9962  acndom  10000  fodomacn  10005  wdomfil  10010  alephon  10018  alephordi  10023  alephle  10037  alephfplem3  10055  dfac2a  10079  kmlem9  10108  cflm  10199  cfslb  10216  cfslbn  10217  infpssrlem3  10255  infpssrlem4  10256  fin23lem21  10289  fin23lem30  10292  isf34lem7  10329  isf34lem6  10330  fin67  10345  isfin7-2  10346  fin1a2lem7  10356  fin1a2lem10  10359  iundom2g  10490  konigthlem  10519  alephreg  10533  gchdomtri  10580  wunr1om  10670  tskr1om  10718  inar1  10726  grur1a  10770  indpi  10858  genpprecl  10952  genpnmax  10958  addcmpblnr  11020  recexsrlem  11054  map2psrpr  11061  ax1rid  11112  axpre-mulgt0  11119  ltle  11264  nnmulcl  12227  nnsub  12250  nn0sub  12524  nneo  12650  uz11  12857  xrltle  13144  xltnegi  13212  xrsupsslem  13303  xrinfmsslem  13304  xrub  13308  supxrunb1  13315  supxrunb2  13316  om2uzuzi  13955  uzrdgxfr  13973  seqcl2  14026  seqfveq2  14030  seqshft2  14034  seqsplit  14041  seqcaopr3  14043  seqf1olem2a  14046  seqid2  14054  seqhomo  14055  ser1const  14064  m1expcl2  14091  expadd  14110  expmul  14113  faclbnd  14296  hashfzp1  14437  hashmap  14441  hashf1lem2  14462  hashf1  14463  seqcoll  14470  wrdsymb0  14555  len0nnbi  14557  eqs1  14619  swrdnd2  14662  wrd2ind  14729  pfxccatin12lem2c  14736  pfxccatin12lem2  14737  swrdccatin1d  14749  repswccat  14792  repswcshw  14818  cshwcshid  14833  rtrclreclem3  15066  rtrclreclem4  15067  dfrtrcl2  15068  relexpindlem  15069  relexpind  15070  rtrclind  15071  recan  15354  rexanre  15364  rlimcn3  15607  caurcvg2  15695  fsumiun  15839  efexp  16123  rpnnen2lem12  16247  dvdstr  16318  alzdvds  16344  zob  16383  sumeven  16411  sumodd  16412  bitsinv1  16466  smu01lem  16509  smupval  16512  smueqlem  16514  smumullem  16516  seq1st  16595  lcmfunsnlem2lem1  16662  lcmfunsnlem2lem2  16663  cncongr2  16692  prmdiveq  16811  odzdvds  16821  pythagtriplem2  16843  pcexp  16885  vdwlem13  17019  ramz  17051  prmolefac  17072  elrestr  17447  xpsff1o  17587  subsubc  17876  clatl  18530  frmdgsum  18886  sursubmefmnd  18920  injsubmefmnd  18921  smndex1mndlem  18936  dfgrp3e  19072  mulgneg2  19140  mulgnnass  19141  mhmmulg  19147  gsumwrev  19396  symgextf1lem  19450  symgfixelsi  19465  pmtrdifellem4  19509  sylow1lem1  19628  efgsfo  19769  efgred  19778  cyggexb  19929  gsumzres  19939  gsum2dlem2  20001  mulgass2  20345  rngimcnv  20491  funcrngcsetc  20676  funcrngcsetcALT  20677  rhmsscrnghm  20701  funcringcsetc  20710  lmodprop2d  20978  lspsnne2  21175  lspsneu  21180  cnfldmulg  21443  cnfldexp  21444  zrhpsgnelbas  21633  assapropd  21910  mplcoe1  22077  mplcoe3  22078  mplcoe5  22080  mhpvarcl  22200  ply1sclf1  22339  mat1scmat  22586  restopn2  23224  cnpf2  23297  cmpfi  23455  txcn  23673  txlm  23695  xkoptsub  23701  xkopjcn  23703  ufildr  23978  cnflf  24049  fclsnei  24066  fclscmp  24077  ufilcmp  24079  cnfcf  24089  symgtgp  24153  isxms2  24495  met2ndc  24570  metustbl  24613  tngngp2  24699  clmmulg  25150  iscau4  25328  ovolunlem1a  25545  ovolicc2lem4  25569  volfiniun  25596  voliunlem1  25599  volsup  25605  dvnadd  25978  dvnres  25980  dvcobr  25995  ply1nzb  26170  plypf1  26259  dgrle  26290  coeaddlem  26296  dgrlt  26313  dvntaylp  26421  cxpmul2  26741  rlimcnp  27017  facgam  27117  wilthlem2  27120  isnsqf  27186  musum  27242  chtub  27263  chpval2  27269  gausslemma2dlem0i  27415  dchrisumlem1  27540  qabvexp  27677  ostthlem2  27679  nodenselem8  27742  lesrec  27879  bday1  27894  sltsleft  27940  sltsright  27941  oncutlt  28344  noseqind  28372  dfnns2  28452  bdaypw2n0bnd  28544  axsegconlem1  29074  ax5seglem4  29089  ax5seglem5  29090  axlowdimlem15  29113  axcontlem2  29122  axcontlem4  29124  incistruhgr  29236  upgredg2vtx  29298  upgredgpr  29299  numedglnl  29301  uhgr2edg  29365  nbupgruvtxres  29564  cusgrfilem1  29612  wlkres  29825  wlkp1lem2  29829  pthdivtx  29883  pthdlem2lem  29923  wlkiswwlks2lem4  30028  wwlksnredwwlkn0  30052  wwlksnextwrd  30053  wwlksnfi  30062  wwlksnextprop  30068  clwlkclwwlklem2a  30156  clwlkclwwlkf1lem2  30163  erclwwlksym  30179  clwwlkf1  30207  eleclclwwlknlem2  30219  erclwwlknsym  30228  clwwlknonex2  30267  eupth2lem3lem6  30391  frgr3vlem1  30431  3vfriswmgrlem  30435  wlkl0  30525  sspval  30882  nmosetre  30923  nmobndseqi  30938  nmobndseqiALT  30939  orthcom  31267  shsva  31479  shmodsi  31548  h1datomi  31740  nmopsetretALT  32022  nmfnsetre  32036  lnopcnbd  32195  pjclem4  32358  pj3si  32366  ssmd1  32470  atom1d  32512  chjatom  32516  atcvat4i  32556  cdj3lem2a  32595  cdj3lem3a  32598  disjunsn  32753  unitdivcld  34158  xrge0iifiso  34192  dya2iocuni  34540  bnj168  34986  bnj535  35145  bnj590  35165  bnj594  35167  bnj938  35192  bnj1118  35239  bnj1128  35245  fnrelpredd  35347  deranglem  35476  subfacp1lem6  35495  subfacval2  35497  cvmlift2lem12  35624  satffun  35719  mrsubvrs  35832  msrrcl  35853  mclsax  35879  dfon2lem6  36096  rdgprc  36102  ifscgr  36354  btwncolinear1  36379  hfelhf  36491  opnrebl2  36641  nn0prpw  36643  ordcmp  36767  findreccl  36773  nndivlub  36778  axtcond  36798  dfttc2g  36826  mh-inf3f1  36861  bj-rest0  37543  bj-isrvec2  37752  topdifinffinlem  37801  iooelexlt  37816  rdgeqoa  37824  exrecfnlem  37833  wl-mo3t  38039  matunitlindflem2  38076  poimirlem2  38081  poimirlem23  38102  poimirlem28  38107  poimirlem29  38108  poimirlem31  38110  poimirlem32  38111  sdclem2  38201  sdclem1  38202  prdsbnd2  38254  ismtyval  38259  rrnequiv  38294  isexid2  38314  ismndo1  38332  exidreslem  38336  rngo2  38366  rngoueqz  38399  risci  38446  eldisjdmqsim  39276  prtlem11  39450  prtlem15  39459  cvrat4  40027  lcfl6  42084  dvdsexpnn0  42903  harval3  44074  clcnvlem  44159  cnvrcl0  44161  cnvtrcl0  44162  iunrelexpmin1  44244  iunrelexpmin2  44248  ormkglobd  47411  fcoresf1b  47624  aovmpt4g  47755  elsetpreimafvbi  47957  iccpartiltu  47988  iccpartgt  47993  iccpartgel  47995  reuopreuprim  48092  fmtnofac1  48139  gbepos  48340  grtrif1o  48524  grtriclwlk3  48527  isubgr3stgrlem4  48551  gpgprismgr4cycllem3  48679  pgnbgreunbgrlem1  48695  pgnbgreunbgrlem3  48700  pgnbgreunbgrlem4  48701  pgnbgreunbgrlem5lem1  48702  pgnbgreunbgrlem5lem2  48703  pgnbgreunbgrlem5lem3  48704  pgnbgreunbgrlem6  48706  pgnbgreunbgr  48707  ellcoellss  49017  dignn0flhalflem2  49198  nn0sumshdiglemB  49202  1arympt1  49220  opth1neg  49407  opth2neg  49408  oppccatb  49597  fullthinc  50031