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  3503  unineq  4240  elpreqprlem  4822  oteqex  5448  otel3xp  5670  eqrelrdv2  5744  breldmg  5858  elrnmpt1  5909  cnveqb  6154  cnveq0  6155  predpoirr  6291  predfrirr  6292  limelon  6382  f1ssf1  6806  ndmfv  6866  eqfnun  6982  ffvresb  7070  isomin  7283  isofrlem  7286  oprabidw  7389  caovord3d  7568  eldifpw  7713  ssonuni  7725  onsucuni2  7776  ordzsl  7787  tfindsg  7803  findsg  7839  oteqimp  7952  frxp  8068  poxp  8070  fnwelem  8073  tfrlem11  8319  ord1eln01  8423  ord2eln012  8424  oacl  8462  omcl  8463  oecl  8464  oa0r  8465  om0r  8466  om1r  8470  oe1m  8472  oaordi  8473  oawordri  8477  oaass  8488  oarec  8489  omwordri  8499  odi  8506  omass  8507  oewordri  8520  oeworde  8521  oeordsuc  8522  oelim2  8523  oeoa  8525  oeoelem  8526  oeoe  8527  nnm0r  8538  nnacl  8539  nnacom  8545  nnaordi  8546  nnaass  8550  nndi  8551  nnmass  8552  nnmsucr  8553  nnmcom  8554  omabs  8579  brecop  8747  eceqoveq  8759  elpm2r  8782  map0g  8822  undifixp  8872  fundmen  8968  mapxpen  9071  mapunen  9074  pssnn  9093  php  9131  unxpdomlem2  9157  f1vrnfibi  9242  elfir  9318  wemapso2lem  9457  wdompwdom  9483  inf3lem1  9537  inf3lem3  9539  cantnfval2  9578  cantnfp1lem3  9589  r1sdom  9686  r1tr  9688  carden2a  9878  fidomtri2  9906  prdom2  9916  infxpenlem  9923  acndom  9961  fodomacn  9966  wdomfil  9971  alephon  9979  alephordi  9984  alephle  9998  alephfplem3  10016  dfac2a  10040  kmlem9  10069  cflm  10160  cfslb  10176  cfslbn  10177  infpssrlem3  10215  infpssrlem4  10216  fin23lem21  10249  fin23lem30  10252  isf34lem7  10289  isf34lem6  10290  fin67  10305  isfin7-2  10306  fin1a2lem7  10316  fin1a2lem10  10319  iundom2g  10450  konigthlem  10479  alephreg  10493  gchdomtri  10540  wunr1om  10630  tskr1om  10678  inar1  10686  grur1a  10730  indpi  10818  genpprecl  10912  genpnmax  10918  addcmpblnr  10980  recexsrlem  11014  map2psrpr  11021  ax1rid  11072  axpre-mulgt0  11079  ltle  11221  nnmulcl  12169  nnsub  12189  nn0sub  12451  nneo  12576  uz11  12776  xrltle  13063  xltnegi  13131  xrsupsslem  13222  xrinfmsslem  13223  xrub  13227  supxrunb1  13234  supxrunb2  13235  om2uzuzi  13872  uzrdgxfr  13890  seqcl2  13943  seqfveq2  13947  seqshft2  13951  seqsplit  13958  seqcaopr3  13960  seqf1olem2a  13963  seqid2  13971  seqhomo  13972  ser1const  13981  m1expcl2  14008  expadd  14027  expmul  14030  faclbnd  14213  hashfzp1  14354  hashmap  14358  hashf1lem2  14379  hashf1  14380  seqcoll  14387  wrdsymb0  14472  len0nnbi  14474  eqs1  14536  swrdnd2  14579  wrd2ind  14646  pfxccatin12lem2c  14653  pfxccatin12lem2  14654  swrdccatin1d  14666  repswccat  14709  repswcshw  14735  cshwcshid  14750  rtrclreclem3  14983  rtrclreclem4  14984  dfrtrcl2  14985  relexpindlem  14986  relexpind  14987  rtrclind  14988  recan  15260  rexanre  15270  rlimcn3  15513  caurcvg2  15601  fsumiun  15744  efexp  16026  rpnnen2lem12  16150  dvdstr  16221  alzdvds  16247  zob  16286  sumeven  16314  sumodd  16315  bitsinv1  16369  smu01lem  16412  smupval  16415  smueqlem  16417  smumullem  16419  seq1st  16498  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  cncongr2  16595  prmdiveq  16713  odzdvds  16723  pythagtriplem2  16745  pcexp  16787  vdwlem13  16921  ramz  16953  prmolefac  16974  elrestr  17348  xpsff1o  17488  subsubc  17777  clatl  18431  frmdgsum  18787  sursubmefmnd  18821  injsubmefmnd  18822  smndex1mndlem  18834  dfgrp3e  18970  mulgneg2  19038  mulgnnass  19039  mhmmulg  19045  gsumwrev  19295  symgextf1lem  19349  symgfixelsi  19364  pmtrdifellem4  19408  sylow1lem1  19527  efgsfo  19668  efgred  19677  cyggexb  19828  gsumzres  19838  gsum2dlem2  19900  mulgass2  20244  rngimcnv  20392  funcrngcsetc  20573  funcrngcsetcALT  20574  rhmsscrnghm  20598  funcringcsetc  20607  lmodprop2d  20875  lspsnne2  21073  lspsneu  21078  cnfldmulg  21358  cnfldexp  21359  zrhpsgnelbas  21549  assapropd  21827  mplcoe1  21992  mplcoe3  21993  mplcoe5  21995  mhpvarcl  22091  ply1sclf1  22231  mat1scmat  22483  restopn2  23121  cnpf2  23194  cmpfi  23352  txcn  23570  txlm  23592  xkoptsub  23598  xkopjcn  23600  ufildr  23875  cnflf  23946  fclsnei  23963  fclscmp  23974  ufilcmp  23976  cnfcf  23986  symgtgp  24050  isxms2  24392  met2ndc  24467  metustbl  24510  tngngp2  24596  clmmulg  25057  iscau4  25235  ovolunlem1a  25453  ovolicc2lem4  25477  volfiniun  25504  voliunlem1  25507  volsup  25513  dvnadd  25887  dvnres  25889  dvcobr  25905  dvcobrOLD  25906  ply1nzb  26084  plypf1  26173  dgrle  26204  coeaddlem  26210  dgrlt  26228  dvntaylp  26335  cxpmul2  26654  rlimcnp  26931  facgam  27032  wilthlem2  27035  isnsqf  27101  musum  27157  chtub  27179  chpval2  27185  gausslemma2dlem0i  27331  dchrisumlem1  27456  qabvexp  27593  ostthlem2  27595  nodenselem8  27659  lesrec  27795  bday1  27810  sltsleft  27856  sltsright  27857  oncutlt  28260  noseqind  28288  dfnns2  28368  bdaypw2n0bnd  28460  axsegconlem1  28990  ax5seglem4  29005  ax5seglem5  29006  axlowdimlem15  29029  axcontlem2  29038  axcontlem4  29040  incistruhgr  29152  upgredg2vtx  29214  upgredgpr  29215  numedglnl  29217  uhgr2edg  29281  nbupgruvtxres  29480  cusgrfilem1  29529  wlkres  29742  wlkp1lem2  29746  pthdivtx  29800  pthdlem2lem  29840  wlkiswwlks2lem4  29945  wwlksnredwwlkn0  29969  wwlksnextwrd  29970  wwlksnfi  29979  wwlksnextprop  29985  clwlkclwwlklem2a  30073  clwlkclwwlkf1lem2  30080  erclwwlksym  30096  clwwlkf1  30124  eleclclwwlknlem2  30136  erclwwlknsym  30145  clwwlknonex2  30184  eupth2lem3lem6  30308  frgr3vlem1  30348  3vfriswmgrlem  30352  wlkl0  30442  sspval  30798  nmosetre  30839  nmobndseqi  30854  nmobndseqiALT  30855  orthcom  31183  shsva  31395  shmodsi  31464  h1datomi  31656  nmopsetretALT  31938  nmfnsetre  31952  lnopcnbd  32111  pjclem4  32274  pj3si  32282  ssmd1  32386  atom1d  32428  chjatom  32432  atcvat4i  32472  cdj3lem2a  32511  cdj3lem3a  32514  disjunsn  32669  unitdivcld  34058  xrge0iifiso  34092  dya2iocuni  34440  bnj168  34886  bnj535  35046  bnj590  35066  bnj594  35068  bnj938  35093  bnj1118  35140  bnj1128  35146  fnrelpredd  35247  deranglem  35360  subfacp1lem6  35379  subfacval2  35381  cvmlift2lem12  35508  satffun  35603  mrsubvrs  35716  msrrcl  35737  mclsax  35763  dfon2lem6  35980  rdgprc  35986  ifscgr  36238  btwncolinear1  36263  hfelhf  36375  opnrebl2  36515  nn0prpw  36517  ordcmp  36641  findreccl  36647  nndivlub  36652  bj-rest0  37294  bj-isrvec2  37501  topdifinffinlem  37548  iooelexlt  37563  rdgeqoa  37571  exrecfnlem  37580  wl-mo3t  37777  matunitlindflem2  37814  poimirlem2  37819  poimirlem23  37840  poimirlem28  37845  poimirlem29  37846  poimirlem31  37848  poimirlem32  37849  sdclem2  37939  sdclem1  37940  prdsbnd2  37992  ismtyval  37997  rrnequiv  38032  isexid2  38052  ismndo1  38070  exidreslem  38074  rngo2  38104  rngoueqz  38137  risci  38184  prtlem11  39122  prtlem15  39131  cvrat4  39699  lcfl6  41756  dvdsexpnn0  42585  harval3  43775  clcnvlem  43860  cnvrcl0  43862  cnvtrcl0  43863  iunrelexpmin1  43945  iunrelexpmin2  43949  ormkglobd  47115  fcoresf1b  47312  aovmpt4g  47443  elsetpreimafvbi  47633  iccpartiltu  47664  iccpartgt  47669  iccpartgel  47671  reuopreuprim  47768  fmtnofac1  47812  gbepos  48000  grtrif1o  48184  grtriclwlk3  48187  isubgr3stgrlem4  48211  gpgprismgr4cycllem3  48339  pgnbgreunbgrlem1  48355  pgnbgreunbgrlem3  48360  pgnbgreunbgrlem4  48361  pgnbgreunbgrlem5lem1  48362  pgnbgreunbgrlem5lem2  48363  pgnbgreunbgrlem5lem3  48364  pgnbgreunbgrlem6  48366  pgnbgreunbgr  48367  ellcoellss  48677  dignn0flhalflem2  48858  nn0sumshdiglemB  48862  1arympt1  48880  opth1neg  49067  opth2neg  49068  oppccatb  49257  fullthinc  49691