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  2447  pm2.61ne  3013  spcimgft  3501  unineq  4238  elpreqprlem  4818  oteqex  5440  otel3xp  5662  eqrelrdv2  5735  breldmg  5849  elrnmpt1  5900  cnveqb  6143  cnveq0  6144  predpoirr  6280  predfrirr  6281  limelon  6371  f1ssf1  6795  ndmfv  6854  eqfnun  6970  ffvresb  7058  isomin  7271  isofrlem  7274  oprabidw  7377  caovord3d  7556  eldifpw  7701  ssonuni  7713  onsucuni2  7764  ordzsl  7775  tfindsg  7791  findsg  7827  oteqimp  7940  frxp  8056  poxp  8058  fnwelem  8061  tfrlem11  8307  ord1eln01  8411  ord2eln012  8412  oacl  8450  omcl  8451  oecl  8452  oa0r  8453  om0r  8454  om1r  8458  oe1m  8460  oaordi  8461  oawordri  8465  oaass  8476  oarec  8477  omwordri  8487  odi  8494  omass  8495  oewordri  8507  oeworde  8508  oeordsuc  8509  oelim2  8510  oeoa  8512  oeoelem  8513  oeoe  8514  nnm0r  8525  nnacl  8526  nnacom  8532  nnaordi  8533  nnaass  8537  nndi  8538  nnmass  8539  nnmsucr  8540  nnmcom  8541  omabs  8566  brecop  8734  eceqoveq  8746  elpm2r  8769  map0g  8808  undifixp  8858  fundmen  8953  mapxpen  9056  mapunen  9059  pssnn  9078  php  9116  unxpdomlem2  9141  f1vrnfibi  9226  elfir  9299  wemapso2lem  9438  wdompwdom  9464  inf3lem1  9518  inf3lem3  9520  cantnfval2  9559  cantnfp1lem3  9570  r1sdom  9664  r1tr  9666  carden2a  9856  fidomtri2  9884  prdom2  9894  infxpenlem  9901  acndom  9939  fodomacn  9944  wdomfil  9949  alephon  9957  alephordi  9962  alephle  9976  alephfplem3  9994  dfac2a  10018  kmlem9  10047  cflm  10138  cfslb  10154  cfslbn  10155  infpssrlem3  10193  infpssrlem4  10194  fin23lem21  10227  fin23lem30  10230  isf34lem7  10267  isf34lem6  10268  fin67  10283  isfin7-2  10284  fin1a2lem7  10294  fin1a2lem10  10297  iundom2g  10428  konigthlem  10456  alephreg  10470  gchdomtri  10517  wunr1om  10607  tskr1om  10655  inar1  10663  grur1a  10707  indpi  10795  genpprecl  10889  genpnmax  10895  addcmpblnr  10957  recexsrlem  10991  map2psrpr  10998  ax1rid  11049  axpre-mulgt0  11056  ltle  11198  nnmulcl  12146  nnsub  12166  nn0sub  12428  nneo  12554  uz11  12754  xrltle  13045  xltnegi  13112  xrsupsslem  13203  xrinfmsslem  13204  xrub  13208  supxrunb1  13215  supxrunb2  13216  om2uzuzi  13853  uzrdgxfr  13871  seqcl2  13924  seqfveq2  13928  seqshft2  13932  seqsplit  13939  seqcaopr3  13941  seqf1olem2a  13944  seqid2  13952  seqhomo  13953  ser1const  13962  m1expcl2  13989  expadd  14008  expmul  14011  faclbnd  14194  hashfzp1  14335  hashmap  14339  hashf1lem2  14360  hashf1  14361  seqcoll  14368  wrdsymb0  14453  len0nnbi  14455  eqs1  14517  swrdnd2  14560  wrd2ind  14627  pfxccatin12lem2c  14634  pfxccatin12lem2  14635  swrdccatin1d  14647  repswccat  14690  repswcshw  14716  cshwcshid  14731  rtrclreclem3  14964  rtrclreclem4  14965  dfrtrcl2  14966  relexpindlem  14967  relexpind  14968  rtrclind  14969  recan  15241  rexanre  15251  rlimcn3  15494  caurcvg2  15582  fsumiun  15725  efexp  16007  rpnnen2lem12  16131  dvdstr  16202  alzdvds  16228  zob  16267  sumeven  16295  sumodd  16296  bitsinv1  16350  smu01lem  16393  smupval  16396  smueqlem  16398  smumullem  16400  seq1st  16479  lcmfunsnlem2lem1  16546  lcmfunsnlem2lem2  16547  cncongr2  16576  prmdiveq  16694  odzdvds  16704  pythagtriplem2  16726  pcexp  16768  vdwlem13  16902  ramz  16934  prmolefac  16955  elrestr  17329  xpsff1o  17468  subsubc  17757  clatl  18411  frmdgsum  18767  sursubmefmnd  18801  injsubmefmnd  18802  smndex1mndlem  18814  dfgrp3e  18950  mulgneg2  19018  mulgnnass  19019  mhmmulg  19025  gsumwrev  19276  symgextf1lem  19330  symgfixelsi  19345  pmtrdifellem4  19389  sylow1lem1  19508  efgsfo  19649  efgred  19658  cyggexb  19809  gsumzres  19819  gsum2dlem2  19881  mulgass2  20225  rngimcnv  20372  funcrngcsetc  20553  funcrngcsetcALT  20554  rhmsscrnghm  20578  funcringcsetc  20587  lmodprop2d  20855  lspsnne2  21053  lspsneu  21058  cnfldmulg  21338  cnfldexp  21339  zrhpsgnelbas  21529  assapropd  21807  mplcoe1  21970  mplcoe3  21971  mplcoe5  21973  mhpvarcl  22061  ply1sclf1  22201  mat1scmat  22452  restopn2  23090  cnpf2  23163  cmpfi  23321  txcn  23539  txlm  23561  xkoptsub  23567  xkopjcn  23569  ufildr  23844  cnflf  23915  fclsnei  23932  fclscmp  23943  ufilcmp  23945  cnfcf  23955  symgtgp  24019  isxms2  24361  met2ndc  24436  metustbl  24479  tngngp2  24565  clmmulg  25026  iscau4  25204  ovolunlem1a  25422  ovolicc2lem4  25446  volfiniun  25473  voliunlem1  25476  volsup  25482  dvnadd  25856  dvnres  25858  dvcobr  25874  dvcobrOLD  25875  ply1nzb  26053  plypf1  26142  dgrle  26173  coeaddlem  26179  dgrlt  26197  dvntaylp  26304  cxpmul2  26623  rlimcnp  26900  facgam  27001  wilthlem2  27004  isnsqf  27070  musum  27126  chtub  27148  chpval2  27154  gausslemma2dlem0i  27300  dchrisumlem1  27425  qabvexp  27562  ostthlem2  27564  nodenselem8  27628  slerec  27758  bday1s  27773  ssltleft  27813  ssltright  27814  onscutlt  28199  noseqind  28220  dfnns2  28295  axsegconlem1  28893  ax5seglem4  28908  ax5seglem5  28909  axlowdimlem15  28932  axcontlem2  28941  axcontlem4  28943  incistruhgr  29055  upgredg2vtx  29117  upgredgpr  29118  numedglnl  29120  uhgr2edg  29184  nbupgruvtxres  29383  cusgrfilem1  29432  wlkres  29645  wlkp1lem2  29649  pthdivtx  29703  pthdlem2lem  29743  wlkiswwlks2lem4  29848  wwlksnredwwlkn0  29872  wwlksnextwrd  29873  wwlksnfi  29882  wwlksnextprop  29888  clwlkclwwlklem2a  29973  clwlkclwwlkf1lem2  29980  erclwwlksym  29996  clwwlkf1  30024  eleclclwwlknlem2  30036  erclwwlknsym  30045  clwwlknonex2  30084  eupth2lem3lem6  30208  frgr3vlem1  30248  3vfriswmgrlem  30252  wlkl0  30342  sspval  30698  nmosetre  30739  nmobndseqi  30754  nmobndseqiALT  30755  orthcom  31083  shsva  31295  shmodsi  31364  h1datomi  31556  nmopsetretALT  31838  nmfnsetre  31852  lnopcnbd  32011  pjclem4  32174  pj3si  32182  ssmd1  32286  atom1d  32328  chjatom  32332  atcvat4i  32372  cdj3lem2a  32411  cdj3lem3a  32414  disjunsn  32569  unitdivcld  33909  xrge0iifiso  33943  dya2iocuni  34291  bnj168  34737  bnj535  34897  bnj590  34917  bnj594  34919  bnj938  34944  bnj1118  34991  bnj1128  34997  fnrelpredd  35097  deranglem  35198  subfacp1lem6  35217  subfacval2  35219  cvmlift2lem12  35346  satffun  35441  mrsubvrs  35554  msrrcl  35575  mclsax  35601  dfon2lem6  35821  rdgprc  35827  ifscgr  36077  btwncolinear1  36102  hfelhf  36214  opnrebl2  36354  nn0prpw  36356  ordcmp  36480  findreccl  36486  nndivlub  36491  bj-rest0  37126  bj-isrvec2  37333  topdifinffinlem  37380  iooelexlt  37395  rdgeqoa  37403  exrecfnlem  37412  wl-mo3t  37609  matunitlindflem2  37656  poimirlem2  37661  poimirlem23  37682  poimirlem28  37687  poimirlem29  37688  poimirlem31  37690  poimirlem32  37691  sdclem2  37781  sdclem1  37782  prdsbnd2  37834  ismtyval  37839  rrnequiv  37874  isexid2  37894  ismndo1  37912  exidreslem  37916  rngo2  37946  rngoueqz  37979  risci  38026  prtlem11  38904  prtlem15  38913  cvrat4  39481  lcfl6  41538  dvdsexpnn0  42366  harval3  43570  clcnvlem  43655  cnvrcl0  43657  cnvtrcl0  43658  iunrelexpmin1  43740  iunrelexpmin2  43744  ormkglobd  46912  fcoresf1b  47100  aovmpt4g  47231  elsetpreimafvbi  47421  iccpartiltu  47452  iccpartgt  47457  iccpartgel  47459  reuopreuprim  47556  fmtnofac1  47600  gbepos  47788  grtrif1o  47972  grtriclwlk3  47975  isubgr3stgrlem4  47999  gpgprismgr4cycllem3  48127  pgnbgreunbgrlem1  48143  pgnbgreunbgrlem3  48148  pgnbgreunbgrlem4  48149  pgnbgreunbgrlem5lem1  48150  pgnbgreunbgrlem5lem2  48151  pgnbgreunbgrlem5lem3  48152  pgnbgreunbgrlem6  48154  pgnbgreunbgr  48155  ellcoellss  48466  dignn0flhalflem2  48647  nn0sumshdiglemB  48651  1arympt1  48669  opth1neg  48856  opth2neg  48857  oppccatb  49047  fullthinc  49481