Theorem syl5ibrcom 246

Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)

Hypotheses

Ref	Expression
imbitrrid.1	⊢ (𝜑 → 𝜃)
imbitrrid.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5ibrcom	⊢ (𝜑 → (𝜒 → 𝜓))

Proof of Theorem syl5ibrcom

Step	Hyp	Ref	Expression
1		imbitrrid.1	. . 3 ⊢ (𝜑 → 𝜃)
2		imbitrrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	imbitrrid 245	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
4	3	com12 32	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:  biimprcd  249  elsn2g  4629  preq1b  4809  elpreqprb  4830  reusv3  5365  alxfr  5367  reuhypd  5379  opth1  5437  euotd  5475  otiunsndisj  5482  tz7.2  5622  frsn  5724  dmopab2rex  5878  elsnxp  6248  reuop  6250  dfpo2  6253  ordtri1  6355  ordtri3  6358  fvmptdv2  6971  fveqressseq  7035  foco2  7062  fsn  7086  fnsnb  7117  fmptsng  7119  fmptsnd  7120  fconst2g  7157  fnprb  7163  fntpb  7164  funfvima  7185  soisoi  7278  isores3  7285  eqfunresadj  7310  riotaeqimp  7345  eusvobj2  7354  ovmpodv2  7518  f1opw2  7613  sorpssun  7672  sorpssin  7673  oneqmin  7740  nlimsucg  7783  onzsl  7787  tfinds  7801  funcnvuni  7873  opiota  7996  mposn  8040  frpoins3xpg  8077  frpoins3xp3g  8078  poxp2  8080  xpord2pred  8082  sexp2  8083  poxp3  8087  xpord3pred  8089  sexp3  8090  xpord3inddlem  8091  suppssov1  8134  suppssfv  8138  brtpos  8171  frrlem12  8233  frrlem13  8234  wfrlem10OLD  8269  wfrlem14OLD  8273  wfrlem15OLD  8274  seqomlem1  8401  seqomlem2  8402  omordi  8518  omord  8520  omwordi  8523  oeeui  8554  nnmordi  8583  nnmord  8584  nnmwordi  8587  nnawordex  8589  nnaordex  8590  nneob  8607  omsmolem  8608  eldifsucnn  8615  qsss  8724  eroveu  8758  mapsncnv  8838  ralxpmap  8841  elixpsn  8882  ixpsnf1o  8883  boxcutc  8886  pw2f1olem  9027  2pwne  9084  mapxpen  9094  mapunen  9097  php  9161  phpOLD  9173  onomeneq  9179  unxpdomlem2  9202  en1eqsnbi  9227  isfiniteg  9255  fofinf1o  9278  f1opwfi  9307  elfiun  9375  oieu  9484  brwdom2  9518  wdomtr  9520  ixpiunwdom  9535  en3lplem1  9557  suc11reg  9564  inf3lemd  9572  cantnfvalf  9610  cantnflt  9617  cantnfp1lem3  9625  cantnflem2  9635  ttrcltr  9661  rnttrcl  9667  ttrclselem1  9670  r1tr  9721  updjud  9879  dfac8alem  9974  wdomnumr  10009  isinfcard  10037  aceq3lem  10065  dfac5lem4  10071  dfac5  10073  dfac2b  10075  coftr  10218  fin23lem28  10285  fin23lem29  10286  fin1a2lem11  10355  fin1a2lem12  10356  fin1a2lem13  10357  hsmexlem9  10370  axdclem  10464  pwcfsdom  10528  gchdomtri  10574  fpwwe2  10588  gchpwdom  10615  gchhar  10624  addnidpi  10846  nqereu  10874  genpv  10944  genpdm  10947  distrlem5pr  10972  mulrid  11162  ltne  11261  mul02  11342  cnegex  11345  mul0or  11804  negfi  12113  sup2  12120  supaddc  12131  supadd  12132  supmul1  12133  supmul  12136  creur  12156  creui  12157  cju  12158  nnsub  12206  un0addcl  12455  un0mulcl  12456  nn0sub  12472  elz2  12526  zaddcl  12552  suprzcl2  12872  qmulz  12885  qre  12887  qnegcl  12900  elpqb  12910  xrmax1  13104  xrmin2  13107  max1ALT  13115  xlesubadd  13192  xmulass  13216  xlemul1a  13217  xrsupexmnf  13234  xrinfmexpnf  13235  xrub  13241  iccid  13319  fzsn  13493  fzsuc2  13509  fz1sbc  13527  elfzp12  13530  modmuladd  13828  seqid3  13962  bcval5  14228  bcpasc  14231  hashbnd  14246  hashnnn0genn0  14253  hashprg  14305  hashfzo  14339  wrdl1s1  14514  ccats1alpha  14519  cats1un  14621  shftlem  14965  replim  15013  absmod0  15200  absz  15208  rlimdm  15445  summolem2  15612  summo  15613  zsum  15614  fsum  15616  fsummulc2  15680  fsumconst  15686  fsum00  15694  incexclem  15732  isumsplit  15736  infcvgaux1i  15753  prodmolem2  15829  prodmo  15830  zprod  15831  fprod  15835  prodsn  15856  prodsnf  15858  fprodconst  15872  ruclem2  16125  fzo0dvdseq  16216  bitsf1ocnv  16335  sadcaddlem  16348  smueqlem  16381  gcdabs1  16420  bezoutlem1  16431  bezoutlem3  16433  bezoutlem4  16434  dvdsgcd  16436  dvdsmulgcd  16447  lcmgcdeq  16499  lcmf  16520  lcmfunsnlem1  16524  lcmfunsnlem2lem2  16526  isprm2lem  16568  dvdsprime  16574  isprm5  16594  coprm  16598  prmdvdsexpr  16604  rpexp  16609  phibndlem  16653  dfphi2  16657  hashgcdlem  16671  odzdvds  16678  nnoddn2prm  16694  pythagtriplem1  16699  iserodd  16718  pceulem  16728  pcqmul  16736  pcqcl  16739  pcxnn0cl  16743  pcxcl  16744  pcneg  16757  pcabs  16758  pcgcd1  16760  pcz  16764  pcprmpw2  16765  pcprmpw  16766  dvdsprmpweqle  16769  difsqpwdvds  16770  pcaddlem  16771  pcadd  16772  pcmpt  16775  pockthg  16789  prmreclem5  16803  4sqlem4  16835  mul4sq  16837  vdwapun  16857  vdwlem2  16865  vdwlem6  16869  vdwlem8  16871  vdwlem13  16876  0ram  16903  ram0  16905  ramcl  16912  cshwsiun  16983  wunress  17145  wunressOLD  17146  firest  17328  isssc  17717  pospo  18248  latnlej  18359  gsumval2a  18554  mnd1id  18612  0subm  18642  mulgnn0p1  18901  mulgnn0ass  18926  cyccom  19010  gicsubgen  19082  symg1bas  19186  snsymgefmndeq  19190  psgnunilem1  19289  psgnunilem2  19291  mndodcongi  19339  oddvdsnn0  19340  odnncl  19341  oddvds  19343  odeq  19346  odeq1  19356  pgpfi2  19402  sylow2a  19415  sylow2blem3  19418  sylow3lem6  19428  lsmelvalm  19447  lsmsubm  19449  lsmsubg  19450  lsmmod  19471  lsmdisj2  19478  efgmnvl  19510  efgtlen  19522  efgs1b  19532  efgrelexlemb  19546  efgredeu  19548  efgcpbllemb  19551  frgpuptinv  19567  frgpup3lem  19573  qusabl  19657  frgpnabllem1  19665  cyggeninv  19674  cyggenod  19675  gsumval3eu  19695  dprdssv  19809  dprdfeq0  19815  dprdsubg  19817  dprddisj2  19832  ablfacrp  19859  pgpfac1lem3  19870  pgpfaclem2  19875  dvreq1  20136  irredn1  20151  nzrunit  20211  drngmul0or  20251  isabvd  20335  abvdom  20353  issrngd  20376  lmodfopnelem2  20416  lss1d  20481  lspsneq0  20530  lbspss  20600  lsmcl  20601  lvecvs0or  20628  lspindpi  20652  lidl1el  20747  lpiss  20779  lidldvgen  20784  rrgeq0  20797  domneq0  20804  qsssubdrg  20893  zringlpirlem1  20920  znfld  21004  znunit  21007  znrrg  21009  cygznlem3  21013  frgpcyg  21017  psgnghm  21021  ipeq0  21079  cssincl  21129  lsmcss  21133  obselocv  21171  dsmmacl  21184  dsmmlss  21187  mplsubrglem  21447  mplmonmul  21474  mplcoe5lem  21477  mhpsclcl  21574  mhpvarcl  21575  coe1tmmul2  21684  coe1tmmul  21685  pf1ind  21758  mat1dimelbas  21857  mdetralt  21994  mdetunilem2  21999  mdetunilem7  22004  mdetunilem9  22006  maducoeval2  22026  chpscmat  22228  chfacfscmulgsum  22246  chfacfpmmulgsum  22250  istopon  22298  eltg3  22349  tgidm  22367  clsval2  22438  opncldf1  22472  restbas  22546  tgrest  22547  restcld  22560  restcldr  22562  restcls  22569  restntr  22570  ordtbas2  22579  ordtbas  22580  ordtrest2lem  22591  ordtrest2  22592  pnfnei  22608  mnfnei  22609  tgcn  22640  cnconst  22672  cnindis  22680  lmss  22686  ordtt1  22767  discmp  22786  1stcrest  22841  2ndcdisj  22844  cldllycmp  22883  txbas  22955  ptpjpre1  22959  ptuni2  22964  ptbasin  22965  ptbasfi  22969  ptopn2  22972  txbasval  22994  ptpjopn  23000  ptclsg  23003  dfac14lem  23005  xkoccn  23007  ptcnp  23010  upxp  23011  ptrescn  23027  txkgen  23040  xkoptsub  23042  xkopt  23043  xkoco1cn  23045  xkoco2cn  23046  xkococn  23048  xkoinjcn  23075  ordthmeolem  23189  ptuncnv  23195  nrmhaus  23214  fbssint  23226  fbfinnfr  23229  fbasrn  23272  isufil2  23296  filufint  23308  rnelfm  23341  fmfnfmlem2  23343  fmfnfmlem3  23344  fmfnfmlem4  23345  fmfnfm  23346  flimtopon  23358  flimclslem  23372  fclstopon  23400  fclscf  23413  flimfnfcls  23416  alexsublem  23432  alexsubALTlem3  23437  alexsubALTlem4  23438  ptcmplem2  23441  tmdgsum2  23484  symgtgp  23494  cldsubg  23499  qustgplem  23509  tgptsmscld  23539  tsmsxplem1  23541  imasdsf1olem  23763  blssps  23814  blss  23815  stdbdxmet  23908  methaus  23913  metrest  23917  nrginvrcn  24093  nmoeq0  24137  blssioo  24195  xrtgioo  24206  xrsxmet  24209  reconnlem1  24226  reconnlem2  24227  xrge0tsms  24234  elcncf1di  24295  iccpnfcnv  24344  evth  24359  lebnumlem1  24361  lebnumlem2  24362  lebnumlem3  24363  nmoleub3  24519  minveclem3b  24829  ivthlem2  24853  ivthlem3  24854  elovolm  24876  ovolmge0  24878  ovoliun  24906  ovolicc2lem3  24920  ovolicc2  24923  voliunlem3  24953  dyaddisj  24997  dyadmax  24999  opnmblALT  25004  ismbfd  25040  ismbf2d  25041  mbfimaopnlem  25056  mbfimaopn2  25058  i1fmullem  25095  i1fres  25107  itg1climres  25116  mbfi1fseqlem4  25120  itg2lcl  25129  itgsplitioo  25239  ellimc2  25278  rolle  25391  dvlip  25394  dvge0  25407  dvne0  25412  lhop1lem  25414  tdeglem4  25461  tdeglem4OLD  25462  degltlem1  25474  deg1nn0clb  25492  deg1lt0  25493  dvdsq1p  25562  ply1rem  25565  fta1g  25569  elply2  25594  plyf  25596  ne0p  25605  plyeq0lem  25608  plypf1  25610  0dgrb  25644  coe1termlem  25656  dgrcolem2  25672  plymul0or  25678  plyrem  25702  fta1  25705  quotcan  25706  aalioulem3  25731  eff1olem  25941  lognegb  25982  eflogeq  25994  argregt0  26002  argrege0  26003  tanarg  26011  cxpexp  26060  cxpeq0  26070  mulcxp  26077  cxpeq  26147  atans2  26318  scvxcvx  26372  dmgmaddn0  26409  isppw2  26501  vmappw  26502  vmacl  26504  efvmacl  26506  isnsqf  26521  mumullem2  26566  sqff1o  26568  dvdsppwf1o  26572  ppiublem1  26587  vmalelog  26590  chtublem  26596  fsumvma  26598  perfectlem2  26615  perfect  26616  bposlem1  26669  lgsmod  26708  lgsne0  26720  lgsdirnn0  26729  lgsqr  26736  lgsdchr  26740  gausslemma2dlem1a  26750  gausslemma2dlem6  26757  lgseisenlem2  26761  lgsquadlem1  26765  lgsquadlem2  26766  2lgslem1b  26777  2sqlem2  26803  mul2sq  26804  2sqlem7  26809  dchrisum0fno1  26896  pntrsumbnd2  26952  ostthlem1  27012  ostth2lem2  27019  ostth3  27023  ostth  27024  nolesgn2ores  27057  nogesgn1ores  27059  nolt02o  27080  nogt01o  27081  nosupbnd2  27101  noinfbnd2lem1  27115  noetasuplem4  27121  noetainflem4  27125  maxs1  27150  mins2  27153  madef  27229  sltlpss  27279  lrrecfr  27298  addsval  27317  addsproplem2  27325  addsunif  27353  negsid  27382  negsunif  27393  mulsproplem6  27427  mulsproplem7  27428  mulsproplem8  27429  mulsproplem9  27430  mulsproplem10  27431  colinearalg  27922  axpasch  27953  axlowdimlem16  27969  axlowdimlem17  27970  axlowdim  27973  axcontlem2  27977  axcontlem4  27979  axcontlem7  27982  lpvtx  28082  edglnl  28157  numedglnl  28158  usgredgop  28184  usgrexmplef  28270  uhgrspansubgrlem  28301  uhgrspan1  28314  nbusgredgeu0  28379  nb3grprlem2  28392  cusgrsize2inds  28464  vtxd0nedgb  28499  rusgrpropnb  28594  upgrwlkvtxedg  28656  wlkp1lem1  28684  wlkp1lem6  28689  wlkp1lem8  28691  usgr2wlkneq  28767  crctcshwlk  28830  crctcsh  28832  iswwlksnon  28861  wlkiswwlks1  28875  wwlksnextbi  28902  wwlksnextproplem2  28918  wspthsnonn0vne  28925  clwlkclwwlklem2  29007  clwwisshclwws  29022  erclwwlktr  29029  clwwlkel  29053  clwwlkext2edg  29063  erclwwlkntr  29078  clwlknf1oclwwlknlem2  29089  clwlknf1oclwwlknlem3  29090  clwlknf1oclwwlkn  29091  clwwlknonccat  29103  0wlkons1  29128  3wlkdlem6  29172  eupth2eucrct  29224  frgrwopreglem2  29320  2clwwlk2clwwlk  29357  wlkl0  29374  nvmul0or  29655  ipasslem5  29840  ipasslem11  29845  hvmul0or  30030  his6  30104  hhssnv  30269  ocsh  30288  ocin  30301  shsidmi  30389  chnlen0  30449  h1de2bi  30559  h1de2ctlem  30560  h1de2ci  30561  spansni  30562  3oalem1  30667  nmcexi  31031  atcveq0  31353  chcv1  31360  cdjreui  31437  cdj3lem2b  31442  xrge0tsmsd  31969  1fldgenq  32160  ccfldextdgrr  32443  ordtrest2NEWlem  32592  ordtrest2NEW  32593  xrge0iifcnv  32603  esumc  32739  esumpcvgval  32766  ballotlemfc0  33181  ballotlemfcc  33182  subfacp1lem4  33864  subfacp1lem5  33865  erdszelem8  33879  sconnpi1  33920  cvmsss2  33955  cvmlift2lem12  33995  satfv0  34039  satfv0fun  34052  satf00  34055  sat1el2xp  34060  fmla0xp  34064  fmlasucdisj  34080  satffunlem1lem1  34083  satffunlem2lem1  34085  dmopab3rexdif  34086  msubco  34212  msubvrs  34241  sinccvglem  34347  untsucf  34368  nnuni  34385  dfrdg2  34456  colineardim1  34722  btwnconn1lem14  34761  segleantisym  34776  colinbtwnle  34779  outsidele  34793  lineunray  34808  linethru  34814  elicc3  34865  opnregcld  34878  cldregopn  34879  fnejoin2  34917  bj-isrvec  35838  dissneqlem  35884  icorempo  35895  relowlssretop  35907  relowlpssretop  35908  rdgssun  35922  finxpsuclem  35941  lindsenlbs  36146  ptrecube  36151  poimirlem6  36157  poimirlem7  36158  poimirlem16  36167  poimirlem17  36168  poimirlem19  36170  poimirlem20  36171  poimirlem21  36172  poimirlem22  36173  poimirlem23  36174  poimirlem24  36175  poimirlem25  36176  poimirlem26  36177  poimirlem27  36178  poimirlem29  36180  poimirlem30  36181  poimirlem31  36182  poimirlem32  36183  itg2addnclem3  36204  ftc1anclem6  36229  dvasin  36235  unirep  36245  sdclem2  36274  ssbnd  36320  prdsbnd  36325  cntotbnd  36328  heibor1lem  36341  rrnequiv  36367  ismndo2  36406  grpoeqdivid  36413  isdrngo3  36491  crngohomfo  36538  0idl  36557  1idl  36558  divrngidl  36560  smprngopr  36584  prnc  36599  ispridlc  36602  riotaclbgBAD  37489  lshpdisj  37522  lsateln0  37530  lsatcveq0  37567  opnlen0  37723  cmtbr4N  37790  cvrnbtwn2  37810  cvrnbtwn4  37814  atcvreq0  37849  cvlatexch1  37871  exatleN  37940  atlelt  37974  ps-2  38014  llnn0  38052  lplnn0N  38083  islpln2a  38084  lvoln0N  38127  islvol2aN  38128  4at  38149  dalemcea  38196  dalem3  38200  pmapglb2N  38307  pmapglb2xN  38308  cdlema1N  38327  cdlemb  38330  paddasslem17  38372  llnexchb2lem  38404  llnexchb2  38405  lhpat3  38582  ltrnid  38671  trlne  38721  cdlemc4  38730  cdleme11h  38802  cdlemednuN  38836  cdlemg1a  39106  tendoeq2  39310  tendoid0  39361  dva1dim  39521  dib1dim  39701  dihlatat  39873  dochkrshp4  39925  dochkr1  40014  lclkrlem2e  40047  lcfrlem16  40094  lcfrlem28  40106  mapd0  40201  hdmap14lem13  40416  fnsnbt  40728  frlmsnic  40786  dvdsexpnn0  40885  reladdrsub  40912  sn-negex12  40943  sn-mullid  40962  sn-mul02  40967  nn0addcom  40977  nn0mulcom  40981  zmulcomlem  40982  mulgt0con1d  40985  mulgt0con2d  40986  sn-sup2  40996  prjspner1  41022  elrfi  41075  mrefg2  41088  eldiophb  41138  eldioph2b  41144  diophin  41153  diophun  41154  rexzrexnn0  41185  eldioph4b  41192  diophren  41194  rencldnfilem  41201  pellexlem6  41215  jm2.19  41375  rmydioph  41396  expdiophlem1  41403  expdioph  41405  lnr2i  41501  lpirlnr  41502  hbtlem2  41509  hbtlem4  41511  hbtlem6  41514  dgrsub2  41520  dgraa0p  41534  rngunsnply  41558  nlimsuc  41835  dfsucon  41917  radcnvrat  42716  pm14.24  42834  addrcom  42877  natlocalincr  45235  afveu  45505  dfafn5b  45513  rlimdmafv  45529  afv2eu  45590  rlimdmafv2  45610  el1fzopredsuc  45677  elsetpreimafvssdm  45698  imasetpreimafvbijlemfo  45717  sprvalpw  45792  prprvalpw  45827  reupr  45834  fmtnofac2lem  45880  proththdlem  45925  perfectALTVlem2  46034  perfectALTV  46035  gbowpos  46071  gbowgt5  46074  gboge9  46076  nnsum4primesodd  46108  nnsum4primesoddALTV  46109  isomuspgr  46146  ringcinv  46450  ringcinvALTV  46474  lincellss  46627  lindsrng01  46669  suppdm  46711  nnpw2pb  46793  0aryfvalel  46840  0aryfvalelfv  46841  itsclc0xyqsolr  46975