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  2449  pm2.61ne  3024  spcimgft  3545  unineq  4293  elpreqprlem  4870  oteqex  5509  elopabrOLD  5572  otel3xp  5734  eqrelrdv2  5807  breldmg  5922  elrnmpt1  5973  cnveqb  6217  cnveq0  6218  predpoirr  6355  predfrirr  6356  limelon  6449  f1ssf1  6880  ndmfv  6941  eqfnun  7056  ffvresb  7144  isomin  7356  isofrlem  7359  oprabidw  7461  caovord3d  7642  eldifpw  7786  ssonuni  7798  onsucuni2  7853  ordzsl  7865  tfindsg  7881  findsg  7919  oteqimp  8031  frxp  8149  poxp  8151  fnwelem  8154  wfrlem14OLD  8360  tfrlem11  8426  ord1eln01  8532  ord2eln012  8533  oacl  8571  omcl  8572  oecl  8573  oa0r  8574  om0r  8575  om1r  8579  oe1m  8581  oaordi  8582  oawordri  8586  oaass  8597  oarec  8598  omwordri  8608  odi  8615  omass  8616  oewordri  8628  oeworde  8629  oeordsuc  8630  oelim2  8631  oeoa  8633  oeoelem  8634  oeoe  8635  nnm0r  8646  nnacl  8647  nnacom  8653  nnaordi  8654  nnaass  8658  nndi  8659  nnmass  8660  nnmsucr  8661  nnmcom  8662  omabs  8687  brecop  8848  eceqoveq  8860  elpm2r  8883  map0g  8922  undifixp  8972  fundmen  9069  mapxpen  9181  mapunen  9184  pssnn  9206  php  9244  phpOLD  9256  unxpdomlem2  9284  f1vrnfibi  9379  elfir  9452  wemapso2lem  9589  wdompwdom  9615  inf3lem1  9665  inf3lem3  9667  cantnfval2  9706  cantnfp1lem3  9717  r1sdom  9811  r1tr  9813  carden2a  10003  fidomtri2  10031  prdom2  10043  infxpenlem  10050  acndom  10088  fodomacn  10093  wdomfil  10098  alephon  10106  alephordi  10111  alephle  10125  alephfplem3  10143  dfac2a  10167  kmlem9  10196  cflm  10287  cfslb  10303  cfslbn  10304  infpssrlem3  10342  infpssrlem4  10343  fin23lem21  10376  fin23lem30  10379  isf34lem7  10416  isf34lem6  10417  fin67  10432  isfin7-2  10433  fin1a2lem7  10443  fin1a2lem10  10446  iundom2g  10577  konigthlem  10605  alephreg  10619  gchdomtri  10666  wunr1om  10756  tskr1om  10804  inar1  10812  grur1a  10856  indpi  10944  genpprecl  11038  genpnmax  11044  addcmpblnr  11106  recexsrlem  11140  map2psrpr  11147  ax1rid  11198  axpre-mulgt0  11205  ltle  11346  nnmulcl  12287  nnsub  12307  nn0sub  12573  nneo  12699  uz11  12900  xrltle  13187  xltnegi  13254  xrsupsslem  13345  xrinfmsslem  13346  xrub  13350  supxrunb1  13357  supxrunb2  13358  om2uzuzi  13986  uzrdgxfr  14004  seqcl2  14057  seqfveq2  14061  seqshft2  14065  seqsplit  14072  seqcaopr3  14074  seqf1olem2a  14077  seqid2  14085  seqhomo  14086  ser1const  14095  m1expcl2  14122  expadd  14141  expmul  14144  faclbnd  14325  hashfzp1  14466  hashmap  14470  hashf1lem2  14491  hashf1  14492  seqcoll  14499  wrdsymb0  14583  len0nnbi  14585  eqs1  14646  swrdnd2  14689  wrd2ind  14757  pfxccatin12lem2c  14764  pfxccatin12lem2  14765  swrdccatin1d  14777  repswccat  14820  repswcshw  14846  cshwcshid  14862  rtrclreclem3  15095  rtrclreclem4  15096  dfrtrcl2  15097  relexpindlem  15098  relexpind  15099  rtrclind  15100  recan  15371  rexanre  15381  rlimcn3  15622  caurcvg2  15710  fsumiun  15853  efexp  16133  rpnnen2lem12  16257  dvdstr  16327  alzdvds  16353  zob  16392  sumeven  16420  sumodd  16421  bitsinv1  16475  smu01lem  16518  smupval  16521  smueqlem  16523  smumullem  16525  seq1st  16604  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  cncongr2  16701  prmdiveq  16819  odzdvds  16828  pythagtriplem2  16850  pcexp  16892  vdwlem13  17026  ramz  17058  prmolefac  17079  elrestr  17474  xpsff1o  17613  subsubc  17903  clatl  18565  frmdgsum  18887  sursubmefmnd  18921  injsubmefmnd  18922  smndex1mndlem  18934  dfgrp3e  19070  mulgneg2  19138  mulgnnass  19139  mhmmulg  19145  gsumwrev  19399  symgextf1lem  19452  symgfixelsi  19467  pmtrdifellem4  19511  sylow1lem1  19630  efgsfo  19771  efgred  19780  cyggexb  19931  gsumzres  19941  gsum2dlem2  20003  mulgass2  20322  rngimcnv  20472  funcrngcsetc  20656  funcrngcsetcALT  20657  rhmsscrnghm  20681  funcringcsetc  20690  lmodprop2d  20938  lspsnne2  21137  lspsneu  21142  cnfldmulg  21433  cnfldexp  21434  zrhpsgnelbas  21629  assapropd  21909  mplcoe1  22072  mplcoe3  22073  mplcoe5  22075  mhpvarcl  22169  ply1sclf1  22307  mat1scmat  22560  restopn2  23200  cnpf2  23273  cmpfi  23431  txcn  23649  txlm  23671  xkoptsub  23677  xkopjcn  23679  ufildr  23954  cnflf  24025  fclsnei  24042  fclscmp  24053  ufilcmp  24055  cnfcf  24065  symgtgp  24129  isxms2  24473  met2ndc  24551  metustbl  24594  tngngp2  24688  clmmulg  25147  iscau4  25326  ovolunlem1a  25544  ovolicc2lem4  25568  volfiniun  25595  voliunlem1  25598  volsup  25604  dvnadd  25979  dvnres  25981  dvcobr  25997  dvcobrOLD  25998  ply1nzb  26176  plypf1  26265  dgrle  26296  coeaddlem  26302  dgrlt  26320  dvntaylp  26427  cxpmul2  26745  rlimcnp  27022  facgam  27123  wilthlem2  27126  isnsqf  27192  musum  27248  chtub  27270  chpval2  27276  gausslemma2dlem0i  27422  dchrisumlem1  27547  qabvexp  27684  ostthlem2  27686  nodenselem8  27750  slerec  27878  bday1s  27890  ssltleft  27923  ssltright  27924  noseqind  28312  dfnns2  28376  axsegconlem1  28946  ax5seglem4  28961  ax5seglem5  28962  axlowdimlem15  28985  axcontlem2  28994  axcontlem4  28996  incistruhgr  29110  upgredg2vtx  29172  upgredgpr  29173  numedglnl  29175  uhgr2edg  29239  nbupgruvtxres  29438  cusgrfilem1  29487  wlkres  29702  wlkp1lem2  29706  pthdivtx  29761  pthdlem2lem  29799  wlkiswwlks2lem4  29901  wwlksnredwwlkn0  29925  wwlksnextwrd  29926  wwlksnfi  29935  wwlksnextprop  29941  clwlkclwwlklem2a  30026  clwlkclwwlkf1lem2  30033  erclwwlksym  30049  clwwlkf1  30077  eleclclwwlknlem2  30089  erclwwlknsym  30098  clwwlknonex2  30137  eupth2lem3lem6  30261  frgr3vlem1  30301  3vfriswmgrlem  30305  wlkl0  30395  sspval  30751  nmosetre  30792  nmobndseqi  30807  nmobndseqiALT  30808  orthcom  31136  shsva  31348  shmodsi  31417  h1datomi  31609  nmopsetretALT  31891  nmfnsetre  31905  lnopcnbd  32064  pjclem4  32227  pj3si  32235  ssmd1  32339  atom1d  32381  chjatom  32385  atcvat4i  32425  cdj3lem2a  32464  cdj3lem3a  32467  disjunsn  32613  unitdivcld  33861  xrge0iifiso  33895  dya2iocuni  34264  bnj168  34722  bnj535  34882  bnj590  34902  bnj594  34904  bnj938  34929  bnj1118  34976  bnj1128  34982  fnrelpredd  35081  deranglem  35150  subfacp1lem6  35169  subfacval2  35171  cvmlift2lem12  35298  satffun  35393  mrsubvrs  35506  msrrcl  35527  mclsax  35553  dfon2lem6  35769  rdgprc  35775  ifscgr  36025  btwncolinear1  36050  hfelhf  36162  opnrebl2  36303  nn0prpw  36305  ordcmp  36429  findreccl  36435  nndivlub  36440  bj-rest0  37075  bj-isrvec2  37282  topdifinffinlem  37329  iooelexlt  37344  rdgeqoa  37352  exrecfnlem  37361  wl-mo3t  37556  matunitlindflem2  37603  poimirlem2  37608  poimirlem23  37629  poimirlem28  37634  poimirlem29  37635  poimirlem31  37637  poimirlem32  37638  sdclem2  37728  sdclem1  37729  prdsbnd2  37781  ismtyval  37786  rrnequiv  37821  isexid2  37841  ismndo1  37859  exidreslem  37863  rngo2  37893  rngoueqz  37926  risci  37973  prtlem11  38847  prtlem15  38856  cvrat4  39425  lcfl6  41482  dvdsexpnn0  42347  harval3  43527  clcnvlem  43612  cnvrcl0  43614  cnvtrcl0  43615  iunrelexpmin1  43697  iunrelexpmin2  43701  tworepnotupword  46839  fcoresf1b  47019  aovmpt4g  47150  elsetpreimafvbi  47315  iccpartiltu  47346  iccpartgt  47351  iccpartgel  47353  reuopreuprim  47450  fmtnofac1  47494  gbepos  47682  grtrif1o  47846  grtriclwlk3  47849  isubgr3stgrlem4  47871  ellcoellss  48280  dignn0flhalflem2  48465  nn0sumshdiglemB  48469  1arympt1  48487  fullthinc  48845