Theorem imbitrrid 245

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  syl5ibrcom  246  biimprd  247  exdistrf  2446  pm2.61ne  3027  unineq  4276  elpreqprlem  4865  oteqex  5499  elopabrOLD  5562  otel3xp  5720  eqrelrdv2  5793  breldmg  5907  elrnmpt1  5955  cnveqb  6192  cnveq0  6193  predpoirr  6331  predfrirr  6332  limelon  6425  f1ssf1  6862  ndmfv  6923  eqfnun  7035  ffvresb  7120  isomin  7330  isofrlem  7333  oprabidw  7436  caovord3d  7613  eldifpw  7751  ssonuni  7763  onsucuni2  7818  ordzsl  7830  tfindsg  7846  findsg  7886  oteqimp  7990  frxp  8108  poxp  8110  fnwelem  8113  suppssOLD  8176  wfrlem14OLD  8318  tfrlem11  8384  ord1eln01  8492  ord2eln012  8493  oacl  8531  omcl  8532  oecl  8533  oa0r  8534  om0r  8535  om1r  8539  oe1m  8541  oaordi  8542  oawordri  8546  oaass  8557  oarec  8558  omwordri  8568  odi  8575  omass  8576  oewordri  8588  oeworde  8589  oeordsuc  8590  oelim2  8591  oeoa  8593  oeoelem  8594  oeoe  8595  nnm0r  8606  nnacl  8607  nnacom  8613  nnaordi  8614  nnaass  8618  nndi  8619  nnmass  8620  nnmsucr  8621  nnmcom  8622  omabs  8646  brecop  8800  eceqoveq  8812  elpm2r  8835  map0g  8874  undifixp  8924  fundmen  9027  mapxpen  9139  mapunen  9142  pssnn  9164  php  9206  phpOLD  9218  unxpdomlem2  9247  pssnnOLD  9261  f1vrnfibi  9333  elfir  9406  wemapso2lem  9543  wdompwdom  9569  inf3lem1  9619  inf3lem3  9621  cantnfval2  9660  cantnfp1lem3  9671  r1sdom  9765  r1tr  9767  carden2a  9957  fidomtri2  9985  prdom2  9997  infxpenlem  10004  acndom  10042  fodomacn  10047  wdomfil  10052  alephon  10060  alephordi  10065  alephle  10079  alephfplem3  10097  dfac2a  10120  kmlem9  10149  cflm  10241  cfslb  10257  cfslbn  10258  infpssrlem3  10296  infpssrlem4  10297  fin23lem21  10330  fin23lem30  10333  isf34lem7  10370  isf34lem6  10371  fin67  10386  isfin7-2  10387  fin1a2lem7  10397  fin1a2lem10  10400  iundom2g  10531  konigthlem  10559  alephreg  10573  gchdomtri  10620  wunr1om  10710  tskr1om  10758  inar1  10766  grur1a  10810  indpi  10898  genpprecl  10992  genpnmax  10998  addcmpblnr  11060  recexsrlem  11094  map2psrpr  11101  ax1rid  11152  axpre-mulgt0  11159  ltle  11298  nnmulcl  12232  nnsub  12252  nn0sub  12518  nneo  12642  uz11  12843  xrltle  13124  xltnegi  13191  xrsupsslem  13282  xrinfmsslem  13283  xrub  13287  supxrunb1  13294  supxrunb2  13295  om2uzuzi  13910  uzrdgxfr  13928  seqcl2  13982  seqfveq2  13986  seqshft2  13990  seqsplit  13997  seqcaopr3  13999  seqf1olem2a  14002  seqid2  14010  seqhomo  14011  ser1const  14020  m1expcl2  14047  expadd  14066  expmul  14069  faclbnd  14246  hashfzp1  14387  hashmap  14391  hashfacenOLD  14410  hashf1lem1OLD  14412  hashf1lem2  14413  hashf1  14414  seqcoll  14421  wrdsymb0  14495  len0nnbi  14497  eqs1  14558  swrdnd2  14601  wrd2ind  14669  pfxccatin12lem2c  14676  pfxccatin12lem2  14677  swrdccatin1d  14689  repswccat  14732  repswcshw  14758  cshwcshid  14774  rtrclreclem3  15003  rtrclreclem4  15004  dfrtrcl2  15005  relexpindlem  15006  relexpind  15007  rtrclind  15008  recan  15279  rexanre  15289  rlimcn3  15530  caurcvg2  15620  fsumiun  15763  efexp  16040  rpnnen2lem12  16164  dvdstr  16233  alzdvds  16259  zob  16298  sumeven  16326  sumodd  16327  bitsinv1  16379  smu01lem  16422  smupval  16425  smueqlem  16427  smumullem  16429  seq1st  16504  lcmfunsnlem2lem1  16571  lcmfunsnlem2lem2  16572  cncongr2  16601  prmdiveq  16715  odzdvds  16724  pythagtriplem2  16746  pcexp  16788  vdwlem13  16922  ramz  16954  prmolefac  16975  elrestr  17370  xpsff1o  17509  subsubc  17799  clatl  18457  frmdgsum  18739  sursubmefmnd  18773  injsubmefmnd  18774  smndex1mndlem  18786  dfgrp3e  18919  mulgneg2  18982  mulgnnass  18983  mhmmulg  18989  gsumwrev  19227  symgextf1lem  19282  symgfixelsi  19297  pmtrdifellem4  19341  sylow1lem1  19460  efgsfo  19601  efgred  19610  cyggexb  19761  gsumzres  19771  gsum2dlem2  19833  mulgass2  20114  lmodprop2d  20526  lspsnne2  20723  lspsneu  20728  cnfldmulg  20969  cnfldexp  20970  zrhpsgnelbas  21138  assapropd  21417  mplcoe1  21583  mplcoe3  21584  mplcoe5  21586  mhpvarcl  21682  ply1sclf1  21802  mat1scmat  22032  restopn2  22672  cnpf2  22745  cmpfi  22903  txcn  23121  txlm  23143  xkoptsub  23149  xkopjcn  23151  ufildr  23426  cnflf  23497  fclsnei  23514  fclscmp  23525  ufilcmp  23527  cnfcf  23537  symgtgp  23601  isxms2  23945  met2ndc  24023  metustbl  24066  tngngp2  24160  clmmulg  24608  iscau4  24787  ovolunlem1a  25004  ovolicc2lem4  25028  volfiniun  25055  voliunlem1  25058  volsup  25064  dvnadd  25437  dvnres  25439  dvcobr  25454  ply1nzb  25631  plypf1  25717  dgrle  25748  coeaddlem  25754  dgrlt  25771  dvntaylp  25874  cxpmul2  26188  rlimcnp  26459  facgam  26559  wilthlem2  26562  isnsqf  26628  musum  26684  chtub  26704  chpval2  26710  gausslemma2dlem0i  26856  dchrisumlem1  26981  qabvexp  27118  ostthlem2  27120  nodenselem8  27183  slerec  27309  bday1s  27321  ssltleft  27354  ssltright  27355  axsegconlem1  28164  ax5seglem4  28179  ax5seglem5  28180  axlowdimlem15  28203  axcontlem2  28212  axcontlem4  28214  incistruhgr  28328  upgredg2vtx  28390  upgredgpr  28391  numedglnl  28393  uhgr2edg  28454  nbupgruvtxres  28653  cusgrfilem1  28701  wlkres  28916  wlkp1lem2  28920  pthdivtx  28975  pthdlem2lem  29013  wlkiswwlks2lem4  29115  wwlksnredwwlkn0  29139  wwlksnextwrd  29140  wwlksnfi  29149  wwlksnextprop  29155  clwlkclwwlklem2a  29240  clwlkclwwlkf1lem2  29247  erclwwlksym  29263  clwwlkf1  29291  eleclclwwlknlem2  29303  erclwwlknsym  29312  clwwlknonex2  29351  eupth2lem3lem6  29475  frgr3vlem1  29515  3vfriswmgrlem  29519  wlkl0  29609  sspval  29963  nmosetre  30004  nmobndseqi  30019  nmobndseqiALT  30020  orthcom  30348  shsva  30560  shmodsi  30629  h1datomi  30821  nmopsetretALT  31103  nmfnsetre  31117  lnopcnbd  31276  pjclem4  31439  pj3si  31447  ssmd1  31551  atom1d  31593  chjatom  31597  atcvat4i  31637  cdj3lem2a  31676  cdj3lem3a  31679  disjunsn  31812  unitdivcld  32869  xrge0iifiso  32903  dya2iocuni  33270  bnj168  33729  bnj535  33889  bnj590  33909  bnj594  33911  bnj938  33936  bnj1118  33983  bnj1128  33989  fnrelpredd  34080  deranglem  34145  subfacp1lem6  34164  subfacval2  34166  cvmlift2lem12  34293  satffun  34388  mrsubvrs  34501  msrrcl  34522  mclsax  34548  dfon2lem6  34748  rdgprc  34754  ifscgr  35004  btwncolinear1  35029  hfelhf  35141  gg-dvcobr  35164  opnrebl2  35194  nn0prpw  35196  ordcmp  35320  findreccl  35326  nndivlub  35331  bj-rest0  35962  bj-isrvec2  36169  topdifinffinlem  36216  iooelexlt  36231  rdgeqoa  36239  exrecfnlem  36248  wl-mo3t  36429  matunitlindflem2  36473  poimirlem2  36478  poimirlem23  36499  poimirlem28  36504  poimirlem29  36505  poimirlem31  36507  poimirlem32  36508  sdclem2  36598  sdclem1  36599  prdsbnd2  36651  ismtyval  36656  rrnequiv  36691  isexid2  36711  ismndo1  36729  exidreslem  36733  rngo2  36763  rngoueqz  36796  risci  36843  prtlem11  37724  prtlem15  37733  cvrat4  38302  lcfl6  40359  dvdsexpnn0  41227  harval3  42274  clcnvlem  42359  cnvrcl0  42361  cnvtrcl0  42362  iunrelexpmin1  42444  iunrelexpmin2  42448  tworepnotupword  45586  fcoresf1b  45766  aovmpt4g  45895  elsetpreimafvbi  46045  iccpartiltu  46076  iccpartgt  46081  iccpartgel  46083  reuopreuprim  46180  fmtnofac1  46224  gbepos  46412  rngimcnv  46690  funcrngcsetc  46849  funcrngcsetcALT  46850  rhmsscrnghm  46877  funcringcsetc  46886  ellcoellss  47069  dignn0flhalflem2  47255  nn0sumshdiglemB  47259  1arympt1  47277  fullthinc  47619