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  2451  pm2.61ne  3017  spcimgft  3525  unineq  4263  elpreqprlem  4842  oteqex  5475  elopabrOLD  5538  otel3xp  5700  eqrelrdv2  5774  breldmg  5889  elrnmpt1  5940  cnveqb  6185  cnveq0  6186  predpoirr  6322  predfrirr  6323  limelon  6417  f1ssf1  6849  ndmfv  6910  eqfnun  7026  ffvresb  7114  isomin  7329  isofrlem  7332  oprabidw  7434  caovord3d  7615  eldifpw  7760  ssonuni  7772  onsucuni2  7826  ordzsl  7838  tfindsg  7854  findsg  7891  oteqimp  8005  frxp  8123  poxp  8125  fnwelem  8128  wfrlem14OLD  8334  tfrlem11  8400  ord1eln01  8506  ord2eln012  8507  oacl  8545  omcl  8546  oecl  8547  oa0r  8548  om0r  8549  om1r  8553  oe1m  8555  oaordi  8556  oawordri  8560  oaass  8571  oarec  8572  omwordri  8582  odi  8589  omass  8590  oewordri  8602  oeworde  8603  oeordsuc  8604  oelim2  8605  oeoa  8607  oeoelem  8608  oeoe  8609  nnm0r  8620  nnacl  8621  nnacom  8627  nnaordi  8628  nnaass  8632  nndi  8633  nnmass  8634  nnmsucr  8635  nnmcom  8636  omabs  8661  brecop  8822  eceqoveq  8834  elpm2r  8857  map0g  8896  undifixp  8946  fundmen  9043  mapxpen  9155  mapunen  9158  pssnn  9180  php  9219  phpOLD  9229  unxpdomlem2  9257  f1vrnfibi  9352  elfir  9425  wemapso2lem  9564  wdompwdom  9590  inf3lem1  9640  inf3lem3  9642  cantnfval2  9681  cantnfp1lem3  9692  r1sdom  9786  r1tr  9788  carden2a  9978  fidomtri2  10006  prdom2  10018  infxpenlem  10025  acndom  10063  fodomacn  10068  wdomfil  10073  alephon  10081  alephordi  10086  alephle  10100  alephfplem3  10118  dfac2a  10142  kmlem9  10171  cflm  10262  cfslb  10278  cfslbn  10279  infpssrlem3  10317  infpssrlem4  10318  fin23lem21  10351  fin23lem30  10354  isf34lem7  10391  isf34lem6  10392  fin67  10407  isfin7-2  10408  fin1a2lem7  10418  fin1a2lem10  10421  iundom2g  10552  konigthlem  10580  alephreg  10594  gchdomtri  10641  wunr1om  10731  tskr1om  10779  inar1  10787  grur1a  10831  indpi  10919  genpprecl  11013  genpnmax  11019  addcmpblnr  11081  recexsrlem  11115  map2psrpr  11122  ax1rid  11173  axpre-mulgt0  11180  ltle  11321  nnmulcl  12262  nnsub  12282  nn0sub  12549  nneo  12675  uz11  12875  xrltle  13163  xltnegi  13230  xrsupsslem  13321  xrinfmsslem  13322  xrub  13326  supxrunb1  13333  supxrunb2  13334  om2uzuzi  13965  uzrdgxfr  13983  seqcl2  14036  seqfveq2  14040  seqshft2  14044  seqsplit  14051  seqcaopr3  14053  seqf1olem2a  14056  seqid2  14064  seqhomo  14065  ser1const  14074  m1expcl2  14101  expadd  14120  expmul  14123  faclbnd  14306  hashfzp1  14447  hashmap  14451  hashf1lem2  14472  hashf1  14473  seqcoll  14480  wrdsymb0  14565  len0nnbi  14567  eqs1  14628  swrdnd2  14671  wrd2ind  14739  pfxccatin12lem2c  14746  pfxccatin12lem2  14747  swrdccatin1d  14759  repswccat  14802  repswcshw  14828  cshwcshid  14844  rtrclreclem3  15077  rtrclreclem4  15078  dfrtrcl2  15079  relexpindlem  15080  relexpind  15081  rtrclind  15082  recan  15353  rexanre  15363  rlimcn3  15604  caurcvg2  15692  fsumiun  15835  efexp  16117  rpnnen2lem12  16241  dvdstr  16311  alzdvds  16337  zob  16376  sumeven  16404  sumodd  16405  bitsinv1  16459  smu01lem  16502  smupval  16505  smueqlem  16507  smumullem  16509  seq1st  16588  lcmfunsnlem2lem1  16655  lcmfunsnlem2lem2  16656  cncongr2  16685  prmdiveq  16803  odzdvds  16813  pythagtriplem2  16835  pcexp  16877  vdwlem13  17011  ramz  17043  prmolefac  17064  elrestr  17440  xpsff1o  17579  subsubc  17864  clatl  18516  frmdgsum  18838  sursubmefmnd  18872  injsubmefmnd  18873  smndex1mndlem  18885  dfgrp3e  19021  mulgneg2  19089  mulgnnass  19090  mhmmulg  19096  gsumwrev  19347  symgextf1lem  19399  symgfixelsi  19414  pmtrdifellem4  19458  sylow1lem1  19577  efgsfo  19718  efgred  19727  cyggexb  19878  gsumzres  19888  gsum2dlem2  19950  mulgass2  20267  rngimcnv  20414  funcrngcsetc  20598  funcrngcsetcALT  20599  rhmsscrnghm  20623  funcringcsetc  20632  lmodprop2d  20879  lspsnne2  21077  lspsneu  21082  cnfldmulg  21364  cnfldexp  21365  zrhpsgnelbas  21552  assapropd  21830  mplcoe1  21993  mplcoe3  21994  mplcoe5  21996  mhpvarcl  22084  ply1sclf1  22224  mat1scmat  22475  restopn2  23113  cnpf2  23186  cmpfi  23344  txcn  23562  txlm  23584  xkoptsub  23590  xkopjcn  23592  ufildr  23867  cnflf  23938  fclsnei  23955  fclscmp  23966  ufilcmp  23968  cnfcf  23978  symgtgp  24042  isxms2  24385  met2ndc  24460  metustbl  24503  tngngp2  24589  clmmulg  25050  iscau4  25229  ovolunlem1a  25447  ovolicc2lem4  25471  volfiniun  25498  voliunlem1  25501  volsup  25507  dvnadd  25881  dvnres  25883  dvcobr  25899  dvcobrOLD  25900  ply1nzb  26078  plypf1  26167  dgrle  26198  coeaddlem  26204  dgrlt  26222  dvntaylp  26329  cxpmul2  26648  rlimcnp  26925  facgam  27026  wilthlem2  27029  isnsqf  27095  musum  27151  chtub  27173  chpval2  27179  gausslemma2dlem0i  27325  dchrisumlem1  27450  qabvexp  27587  ostthlem2  27589  nodenselem8  27653  slerec  27781  bday1s  27793  ssltleft  27826  ssltright  27827  noseqind  28215  dfnns2  28279  axsegconlem1  28842  ax5seglem4  28857  ax5seglem5  28858  axlowdimlem15  28881  axcontlem2  28890  axcontlem4  28892  incistruhgr  29004  upgredg2vtx  29066  upgredgpr  29067  numedglnl  29069  uhgr2edg  29133  nbupgruvtxres  29332  cusgrfilem1  29381  wlkres  29596  wlkp1lem2  29600  pthdivtx  29655  pthdlem2lem  29695  wlkiswwlks2lem4  29800  wwlksnredwwlkn0  29824  wwlksnextwrd  29825  wwlksnfi  29834  wwlksnextprop  29840  clwlkclwwlklem2a  29925  clwlkclwwlkf1lem2  29932  erclwwlksym  29948  clwwlkf1  29976  eleclclwwlknlem2  29988  erclwwlknsym  29997  clwwlknonex2  30036  eupth2lem3lem6  30160  frgr3vlem1  30200  3vfriswmgrlem  30204  wlkl0  30294  sspval  30650  nmosetre  30691  nmobndseqi  30706  nmobndseqiALT  30707  orthcom  31035  shsva  31247  shmodsi  31316  h1datomi  31508  nmopsetretALT  31790  nmfnsetre  31804  lnopcnbd  31963  pjclem4  32126  pj3si  32134  ssmd1  32238  atom1d  32280  chjatom  32284  atcvat4i  32324  cdj3lem2a  32363  cdj3lem3a  32366  disjunsn  32521  unitdivcld  33878  xrge0iifiso  33912  dya2iocuni  34261  bnj168  34707  bnj535  34867  bnj590  34887  bnj594  34889  bnj938  34914  bnj1118  34961  bnj1128  34967  fnrelpredd  35066  deranglem  35134  subfacp1lem6  35153  subfacval2  35155  cvmlift2lem12  35282  satffun  35377  mrsubvrs  35490  msrrcl  35511  mclsax  35537  dfon2lem6  35752  rdgprc  35758  ifscgr  36008  btwncolinear1  36033  hfelhf  36145  opnrebl2  36285  nn0prpw  36287  ordcmp  36411  findreccl  36417  nndivlub  36422  bj-rest0  37057  bj-isrvec2  37264  topdifinffinlem  37311  iooelexlt  37326  rdgeqoa  37334  exrecfnlem  37343  wl-mo3t  37540  matunitlindflem2  37587  poimirlem2  37592  poimirlem23  37613  poimirlem28  37618  poimirlem29  37619  poimirlem31  37621  poimirlem32  37622  sdclem2  37712  sdclem1  37713  prdsbnd2  37765  ismtyval  37770  rrnequiv  37805  isexid2  37825  ismndo1  37843  exidreslem  37847  rngo2  37877  rngoueqz  37910  risci  37957  prtlem11  38830  prtlem15  38839  cvrat4  39408  lcfl6  41465  dvdsexpnn0  42330  harval3  43509  clcnvlem  43594  cnvrcl0  43596  cnvtrcl0  43597  iunrelexpmin1  43679  iunrelexpmin2  43683  ormkglobd  46852  tworepnotupword  46863  fcoresf1b  47047  aovmpt4g  47178  elsetpreimafvbi  47353  iccpartiltu  47384  iccpartgt  47389  iccpartgel  47391  reuopreuprim  47488  fmtnofac1  47532  gbepos  47720  grtrif1o  47902  grtriclwlk3  47905  isubgr3stgrlem4  47929  gpgprismgr4cycllem3  48044  ellcoellss  48359  dignn0flhalflem2  48544  nn0sumshdiglemB  48548  1arympt1  48566  opth1neg  48752  opth2neg  48753  oppccatb  48939  fullthinc  49284