Theorem imbitrrid 247

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  syl5ibrcom  248  biimprd  249  exdistrf  2455  pm2.61ne  3020  spcimgft  3494  unineq  4223  elpreqprlem  4804  oteqex  5448  otel3xp  5671  eqrelrdv2  5745  breldmg  5858  elrnmpt1  5909  cnveqb  6154  cnveq0  6155  predpoirr  6291  predfrirr  6292  limelon  6382  f1ssf1  6806  ndmfv  6866  eqfnun  6985  ffvresb  7074  isomin  7288  isofrlem  7291  oprabidw  7394  caovord3d  7573  eldifpw  7718  ssonuni  7730  onsucuni2  7781  ordzsl  7792  tfindsg  7808  findsg  7844  oteqimp  7957  frxp  8073  poxp  8075  fnwelem  8078  tfrlem11  8324  ord1eln01  8428  ord2eln012  8429  oacl  8467  omcl  8468  oecl  8469  oa0r  8470  om0r  8471  om1r  8475  oe1m  8477  oaordi  8478  oawordri  8482  oaass  8493  oarec  8494  omwordri  8504  odi  8511  omass  8512  oewordri  8525  oeworde  8526  oeordsuc  8527  oelim2  8528  oeoa  8530  oeoelem  8531  oeoe  8532  nnm0r  8543  nnacl  8544  nnacom  8550  nnaordi  8551  nnaass  8555  nndi  8556  nnmass  8557  nnmsucr  8558  nnmcom  8559  omabs  8584  brecop  8754  eceqoveq  8766  elpm2r  8789  map0g  8829  undifixp  8879  fundmen  8975  mapxpen  9078  mapunen  9081  pssnn  9100  php  9138  unxpdomlem2  9164  f1vrnfibi  9249  elfir  9325  wemapso2lem  9464  wdompwdom  9490  inf3lem1  9547  inf3lem3  9549  cantnfval2  9588  cantnfp1lem3  9599  r1sdom  9696  r1tr  9698  carden2a  9888  fidomtri2  9916  prdom2  9926  infxpenlem  9933  acndom  9971  fodomacn  9976  wdomfil  9981  alephon  9989  alephordi  9994  alephle  10008  alephfplem3  10026  dfac2a  10050  kmlem9  10079  cflm  10170  cfslb  10186  cfslbn  10187  infpssrlem3  10225  infpssrlem4  10226  fin23lem21  10259  fin23lem30  10262  isf34lem7  10299  isf34lem6  10300  fin67  10315  isfin7-2  10316  fin1a2lem7  10326  fin1a2lem10  10329  iundom2g  10460  konigthlem  10489  alephreg  10503  gchdomtri  10550  wunr1om  10640  tskr1om  10688  inar1  10696  grur1a  10740  indpi  10828  genpprecl  10922  genpnmax  10928  addcmpblnr  10990  recexsrlem  11024  map2psrpr  11031  ax1rid  11082  axpre-mulgt0  11089  ltle  11232  nnmulcl  12196  nnsub  12219  nn0sub  12485  nneo  12611  uz11  12811  xrltle  13098  xltnegi  13166  xrsupsslem  13257  xrinfmsslem  13258  xrub  13262  supxrunb1  13269  supxrunb2  13270  om2uzuzi  13909  uzrdgxfr  13927  seqcl2  13980  seqfveq2  13984  seqshft2  13988  seqsplit  13995  seqcaopr3  13997  seqf1olem2a  14000  seqid2  14008  seqhomo  14009  ser1const  14018  m1expcl2  14045  expadd  14064  expmul  14067  faclbnd  14250  hashfzp1  14391  hashmap  14395  hashf1lem2  14416  hashf1  14417  seqcoll  14424  wrdsymb0  14509  len0nnbi  14511  eqs1  14573  swrdnd2  14616  wrd2ind  14683  pfxccatin12lem2c  14690  pfxccatin12lem2  14691  swrdccatin1d  14703  repswccat  14746  repswcshw  14772  cshwcshid  14787  rtrclreclem3  15020  rtrclreclem4  15021  dfrtrcl2  15022  relexpindlem  15023  relexpind  15024  rtrclind  15025  recan  15297  rexanre  15307  rlimcn3  15550  caurcvg2  15638  fsumiun  15782  efexp  16066  rpnnen2lem12  16190  dvdstr  16261  alzdvds  16287  zob  16326  sumeven  16354  sumodd  16355  bitsinv1  16409  smu01lem  16452  smupval  16455  smueqlem  16457  smumullem  16459  seq1st  16538  lcmfunsnlem2lem1  16605  lcmfunsnlem2lem2  16606  cncongr2  16635  prmdiveq  16754  odzdvds  16764  pythagtriplem2  16786  pcexp  16828  vdwlem13  16962  ramz  16994  prmolefac  17015  elrestr  17389  xpsff1o  17529  subsubc  17818  clatl  18472  frmdgsum  18828  sursubmefmnd  18862  injsubmefmnd  18863  smndex1mndlem  18878  dfgrp3e  19014  mulgneg2  19082  mulgnnass  19083  mhmmulg  19089  gsumwrev  19339  symgextf1lem  19393  symgfixelsi  19408  pmtrdifellem4  19452  sylow1lem1  19571  efgsfo  19712  efgred  19721  cyggexb  19872  gsumzres  19882  gsum2dlem2  19944  mulgass2  20288  rngimcnv  20434  funcrngcsetc  20619  funcrngcsetcALT  20620  rhmsscrnghm  20644  funcringcsetc  20653  lmodprop2d  20921  lspsnne2  21118  lspsneu  21123  cnfldmulg  21386  cnfldexp  21387  zrhpsgnelbas  21576  assapropd  21853  mplcoe1  22020  mplcoe3  22021  mplcoe5  22023  mhpvarcl  22143  ply1sclf1  22282  mat1scmat  22529  restopn2  23167  cnpf2  23240  cmpfi  23398  txcn  23616  txlm  23638  xkoptsub  23644  xkopjcn  23646  ufildr  23921  cnflf  23992  fclsnei  24009  fclscmp  24020  ufilcmp  24022  cnfcf  24032  symgtgp  24096  isxms2  24438  met2ndc  24513  metustbl  24556  tngngp2  24642  clmmulg  25093  iscau4  25271  ovolunlem1a  25488  ovolicc2lem4  25512  volfiniun  25539  voliunlem1  25542  volsup  25548  dvnadd  25921  dvnres  25923  dvcobr  25938  ply1nzb  26113  plypf1  26202  dgrle  26233  coeaddlem  26239  dgrlt  26256  dvntaylp  26361  cxpmul2  26678  rlimcnp  26954  facgam  27054  wilthlem2  27057  isnsqf  27123  musum  27179  chtub  27200  chpval2  27206  gausslemma2dlem0i  27352  dchrisumlem1  27477  qabvexp  27614  ostthlem2  27616  nodenselem8  27680  lesrec  27816  bday1  27831  sltsleft  27877  sltsright  27878  oncutlt  28281  noseqind  28309  dfnns2  28389  bdaypw2n0bnd  28481  axsegconlem1  29011  ax5seglem4  29026  ax5seglem5  29027  axlowdimlem15  29050  axcontlem2  29059  axcontlem4  29061  incistruhgr  29173  upgredg2vtx  29235  upgredgpr  29236  numedglnl  29238  uhgr2edg  29302  nbupgruvtxres  29501  cusgrfilem1  29549  wlkres  29762  wlkp1lem2  29766  pthdivtx  29820  pthdlem2lem  29860  wlkiswwlks2lem4  29965  wwlksnredwwlkn0  29989  wwlksnextwrd  29990  wwlksnfi  29999  wwlksnextprop  30005  clwlkclwwlklem2a  30093  clwlkclwwlkf1lem2  30100  erclwwlksym  30116  clwwlkf1  30144  eleclclwwlknlem2  30156  erclwwlknsym  30165  clwwlknonex2  30204  eupth2lem3lem6  30328  frgr3vlem1  30368  3vfriswmgrlem  30372  wlkl0  30462  sspval  30819  nmosetre  30860  nmobndseqi  30875  nmobndseqiALT  30876  orthcom  31204  shsva  31416  shmodsi  31485  h1datomi  31677  nmopsetretALT  31959  nmfnsetre  31973  lnopcnbd  32132  pjclem4  32295  pj3si  32303  ssmd1  32407  atom1d  32449  chjatom  32453  atcvat4i  32493  cdj3lem2a  32532  cdj3lem3a  32535  disjunsn  32690  unitdivcld  34092  xrge0iifiso  34126  dya2iocuni  34474  bnj168  34920  bnj535  35079  bnj590  35099  bnj594  35101  bnj938  35126  bnj1118  35173  bnj1128  35179  fnrelpredd  35279  deranglem  35401  subfacp1lem6  35420  subfacval2  35422  cvmlift2lem12  35549  satffun  35644  mrsubvrs  35757  msrrcl  35778  mclsax  35804  dfon2lem6  36021  rdgprc  36027  ifscgr  36279  btwncolinear1  36304  hfelhf  36416  opnrebl2  36556  nn0prpw  36558  ordcmp  36682  findreccl  36688  nndivlub  36693  axtcond  36713  dfttc2g  36741  mh-inf3f1  36776  bj-rest0  37458  bj-isrvec2  37667  topdifinffinlem  37716  iooelexlt  37731  rdgeqoa  37739  exrecfnlem  37748  wl-mo3t  37954  matunitlindflem2  37991  poimirlem2  37996  poimirlem23  38017  poimirlem28  38022  poimirlem29  38023  poimirlem31  38025  poimirlem32  38026  sdclem2  38116  sdclem1  38117  prdsbnd2  38169  ismtyval  38174  rrnequiv  38209  isexid2  38229  ismndo1  38247  exidreslem  38251  rngo2  38281  rngoueqz  38314  risci  38361  eldisjdmqsim  39191  prtlem11  39365  prtlem15  39374  cvrat4  39942  lcfl6  41999  dvdsexpnn0  42818  harval3  43989  clcnvlem  44074  cnvrcl0  44076  cnvtrcl0  44077  iunrelexpmin1  44159  iunrelexpmin2  44163  ormkglobd  47327  fcoresf1b  47540  aovmpt4g  47671  elsetpreimafvbi  47873  iccpartiltu  47904  iccpartgt  47909  iccpartgel  47911  reuopreuprim  48008  fmtnofac1  48055  gbepos  48256  grtrif1o  48440  grtriclwlk3  48443  isubgr3stgrlem4  48467  gpgprismgr4cycllem3  48595  pgnbgreunbgrlem1  48611  pgnbgreunbgrlem3  48616  pgnbgreunbgrlem4  48617  pgnbgreunbgrlem5lem1  48618  pgnbgreunbgrlem5lem2  48619  pgnbgreunbgrlem5lem3  48620  pgnbgreunbgrlem6  48622  pgnbgreunbgr  48623  ellcoellss  48933  dignn0flhalflem2  49114  nn0sumshdiglemB  49118  1arympt1  49136  opth1neg  49323  opth2neg  49324  oppccatb  49513  fullthinc  49947