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  2452  pm2.61ne  3027  spcimgft  3546  unineq  4288  elpreqprlem  4866  oteqex  5505  elopabrOLD  5568  otel3xp  5731  eqrelrdv2  5805  breldmg  5920  elrnmpt1  5971  cnveqb  6216  cnveq0  6217  predpoirr  6354  predfrirr  6355  limelon  6448  f1ssf1  6880  ndmfv  6941  eqfnun  7057  ffvresb  7145  isomin  7357  isofrlem  7360  oprabidw  7462  caovord3d  7643  eldifpw  7788  ssonuni  7800  onsucuni2  7854  ordzsl  7866  tfindsg  7882  findsg  7919  oteqimp  8033  frxp  8151  poxp  8153  fnwelem  8156  wfrlem14OLD  8362  tfrlem11  8428  ord1eln01  8534  ord2eln012  8535  oacl  8573  omcl  8574  oecl  8575  oa0r  8576  om0r  8577  om1r  8581  oe1m  8583  oaordi  8584  oawordri  8588  oaass  8599  oarec  8600  omwordri  8610  odi  8617  omass  8618  oewordri  8630  oeworde  8631  oeordsuc  8632  oelim2  8633  oeoa  8635  oeoelem  8636  oeoe  8637  nnm0r  8648  nnacl  8649  nnacom  8655  nnaordi  8656  nnaass  8660  nndi  8661  nnmass  8662  nnmsucr  8663  nnmcom  8664  omabs  8689  brecop  8850  eceqoveq  8862  elpm2r  8885  map0g  8924  undifixp  8974  fundmen  9071  mapxpen  9183  mapunen  9186  pssnn  9208  php  9247  phpOLD  9259  unxpdomlem2  9287  f1vrnfibi  9382  elfir  9455  wemapso2lem  9592  wdompwdom  9618  inf3lem1  9668  inf3lem3  9670  cantnfval2  9709  cantnfp1lem3  9720  r1sdom  9814  r1tr  9816  carden2a  10006  fidomtri2  10034  prdom2  10046  infxpenlem  10053  acndom  10091  fodomacn  10096  wdomfil  10101  alephon  10109  alephordi  10114  alephle  10128  alephfplem3  10146  dfac2a  10170  kmlem9  10199  cflm  10290  cfslb  10306  cfslbn  10307  infpssrlem3  10345  infpssrlem4  10346  fin23lem21  10379  fin23lem30  10382  isf34lem7  10419  isf34lem6  10420  fin67  10435  isfin7-2  10436  fin1a2lem7  10446  fin1a2lem10  10449  iundom2g  10580  konigthlem  10608  alephreg  10622  gchdomtri  10669  wunr1om  10759  tskr1om  10807  inar1  10815  grur1a  10859  indpi  10947  genpprecl  11041  genpnmax  11047  addcmpblnr  11109  recexsrlem  11143  map2psrpr  11150  ax1rid  11201  axpre-mulgt0  11208  ltle  11349  nnmulcl  12290  nnsub  12310  nn0sub  12576  nneo  12702  uz11  12903  xrltle  13191  xltnegi  13258  xrsupsslem  13349  xrinfmsslem  13350  xrub  13354  supxrunb1  13361  supxrunb2  13362  om2uzuzi  13990  uzrdgxfr  14008  seqcl2  14061  seqfveq2  14065  seqshft2  14069  seqsplit  14076  seqcaopr3  14078  seqf1olem2a  14081  seqid2  14089  seqhomo  14090  ser1const  14099  m1expcl2  14126  expadd  14145  expmul  14148  faclbnd  14329  hashfzp1  14470  hashmap  14474  hashf1lem2  14495  hashf1  14496  seqcoll  14503  wrdsymb0  14587  len0nnbi  14589  eqs1  14650  swrdnd2  14693  wrd2ind  14761  pfxccatin12lem2c  14768  pfxccatin12lem2  14769  swrdccatin1d  14781  repswccat  14824  repswcshw  14850  cshwcshid  14866  rtrclreclem3  15099  rtrclreclem4  15100  dfrtrcl2  15101  relexpindlem  15102  relexpind  15103  rtrclind  15104  recan  15375  rexanre  15385  rlimcn3  15626  caurcvg2  15714  fsumiun  15857  efexp  16137  rpnnen2lem12  16261  dvdstr  16331  alzdvds  16357  zob  16396  sumeven  16424  sumodd  16425  bitsinv1  16479  smu01lem  16522  smupval  16525  smueqlem  16527  smumullem  16529  seq1st  16608  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  cncongr2  16705  prmdiveq  16823  odzdvds  16833  pythagtriplem2  16855  pcexp  16897  vdwlem13  17031  ramz  17063  prmolefac  17084  elrestr  17473  xpsff1o  17612  subsubc  17898  clatl  18553  frmdgsum  18875  sursubmefmnd  18909  injsubmefmnd  18910  smndex1mndlem  18922  dfgrp3e  19058  mulgneg2  19126  mulgnnass  19127  mhmmulg  19133  gsumwrev  19385  symgextf1lem  19438  symgfixelsi  19453  pmtrdifellem4  19497  sylow1lem1  19616  efgsfo  19757  efgred  19766  cyggexb  19917  gsumzres  19927  gsum2dlem2  19989  mulgass2  20306  rngimcnv  20456  funcrngcsetc  20640  funcrngcsetcALT  20641  rhmsscrnghm  20665  funcringcsetc  20674  lmodprop2d  20922  lspsnne2  21120  lspsneu  21125  cnfldmulg  21416  cnfldexp  21417  zrhpsgnelbas  21612  assapropd  21892  mplcoe1  22055  mplcoe3  22056  mplcoe5  22058  mhpvarcl  22152  ply1sclf1  22292  mat1scmat  22545  restopn2  23185  cnpf2  23258  cmpfi  23416  txcn  23634  txlm  23656  xkoptsub  23662  xkopjcn  23664  ufildr  23939  cnflf  24010  fclsnei  24027  fclscmp  24038  ufilcmp  24040  cnfcf  24050  symgtgp  24114  isxms2  24458  met2ndc  24536  metustbl  24579  tngngp2  24673  clmmulg  25134  iscau4  25313  ovolunlem1a  25531  ovolicc2lem4  25555  volfiniun  25582  voliunlem1  25585  volsup  25591  dvnadd  25965  dvnres  25967  dvcobr  25983  dvcobrOLD  25984  ply1nzb  26162  plypf1  26251  dgrle  26282  coeaddlem  26288  dgrlt  26306  dvntaylp  26413  cxpmul2  26731  rlimcnp  27008  facgam  27109  wilthlem2  27112  isnsqf  27178  musum  27234  chtub  27256  chpval2  27262  gausslemma2dlem0i  27408  dchrisumlem1  27533  qabvexp  27670  ostthlem2  27672  nodenselem8  27736  slerec  27864  bday1s  27876  ssltleft  27909  ssltright  27910  noseqind  28298  dfnns2  28362  axsegconlem1  28932  ax5seglem4  28947  ax5seglem5  28948  axlowdimlem15  28971  axcontlem2  28980  axcontlem4  28982  incistruhgr  29096  upgredg2vtx  29158  upgredgpr  29159  numedglnl  29161  uhgr2edg  29225  nbupgruvtxres  29424  cusgrfilem1  29473  wlkres  29688  wlkp1lem2  29692  pthdivtx  29747  pthdlem2lem  29787  wlkiswwlks2lem4  29892  wwlksnredwwlkn0  29916  wwlksnextwrd  29917  wwlksnfi  29926  wwlksnextprop  29932  clwlkclwwlklem2a  30017  clwlkclwwlkf1lem2  30024  erclwwlksym  30040  clwwlkf1  30068  eleclclwwlknlem2  30080  erclwwlknsym  30089  clwwlknonex2  30128  eupth2lem3lem6  30252  frgr3vlem1  30292  3vfriswmgrlem  30296  wlkl0  30386  sspval  30742  nmosetre  30783  nmobndseqi  30798  nmobndseqiALT  30799  orthcom  31127  shsva  31339  shmodsi  31408  h1datomi  31600  nmopsetretALT  31882  nmfnsetre  31896  lnopcnbd  32055  pjclem4  32218  pj3si  32226  ssmd1  32330  atom1d  32372  chjatom  32376  atcvat4i  32416  cdj3lem2a  32455  cdj3lem3a  32458  disjunsn  32607  unitdivcld  33900  xrge0iifiso  33934  dya2iocuni  34285  bnj168  34744  bnj535  34904  bnj590  34924  bnj594  34926  bnj938  34951  bnj1118  34998  bnj1128  35004  fnrelpredd  35103  deranglem  35171  subfacp1lem6  35190  subfacval2  35192  cvmlift2lem12  35319  satffun  35414  mrsubvrs  35527  msrrcl  35548  mclsax  35574  dfon2lem6  35789  rdgprc  35795  ifscgr  36045  btwncolinear1  36070  hfelhf  36182  opnrebl2  36322  nn0prpw  36324  ordcmp  36448  findreccl  36454  nndivlub  36459  bj-rest0  37094  bj-isrvec2  37301  topdifinffinlem  37348  iooelexlt  37363  rdgeqoa  37371  exrecfnlem  37380  wl-mo3t  37577  matunitlindflem2  37624  poimirlem2  37629  poimirlem23  37650  poimirlem28  37655  poimirlem29  37656  poimirlem31  37658  poimirlem32  37659  sdclem2  37749  sdclem1  37750  prdsbnd2  37802  ismtyval  37807  rrnequiv  37842  isexid2  37862  ismndo1  37880  exidreslem  37884  rngo2  37914  rngoueqz  37947  risci  37994  prtlem11  38867  prtlem15  38876  cvrat4  39445  lcfl6  41502  dvdsexpnn0  42369  harval3  43551  clcnvlem  43636  cnvrcl0  43638  cnvtrcl0  43639  iunrelexpmin1  43721  iunrelexpmin2  43725  ormkglobd  46890  tworepnotupword  46901  fcoresf1b  47082  aovmpt4g  47213  elsetpreimafvbi  47378  iccpartiltu  47409  iccpartgt  47414  iccpartgel  47416  reuopreuprim  47513  fmtnofac1  47557  gbepos  47745  grtrif1o  47909  grtriclwlk3  47912  isubgr3stgrlem4  47936  ellcoellss  48352  dignn0flhalflem2  48537  nn0sumshdiglemB  48541  1arympt1  48559  opth1neg  48739  opth2neg  48740  fullthinc  49099