Theorem syl5ibrcom 247

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 246	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
4	3	com12 32	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:  biimprcd  250  iftrueb  4480  elsn2g  4609  preq1b  4790  elpreqprb  4812  reusv3  5342  alxfr  5344  reuhypd  5356  axpr  5364  opth1  5423  euotd  5461  otiunsndisj  5468  tz7.2  5607  frsn  5712  dmopab2rex  5866  elsnxp  6249  reuop  6251  dfpo2  6254  ordtri1  6350  ordtri3  6353  fvmptdv2  6960  fveqressseq  7025  foco2  7055  fsn  7082  fnsnbg  7112  fnsnbOLD  7114  fmptsng  7116  fmptsnd  7117  fconst2g  7151  fnprb  7156  fntpb  7157  funfvima  7178  soisoi  7276  isores3  7283  eqfunresadj  7308  riotaeqimp  7343  eusvobj2  7352  ovmpodv2  7518  f1opw2  7615  sorpssun  7677  sorpssin  7678  oneqmin  7747  nlimsucg  7786  onzsl  7790  tfinds  7804  funcnvuni  7876  mptcnfimad  7932  opiota  8005  mposn  8046  frpoins3xpg  8083  frpoins3xp3g  8084  poxp2  8086  xpord2pred  8088  sexp2  8089  poxp3  8093  xpord3pred  8095  sexp3  8096  xpord3inddlem  8097  suppssov1  8140  suppssov2  8141  suppssfv  8145  brtpos  8178  frrlem12  8240  frrlem13  8241  seqomlem1  8382  seqomlem2  8383  omordi  8494  omord  8496  omwordi  8499  oeeui  8531  nnmordi  8560  nnmord  8561  nnmwordi  8564  nnawordex  8566  nnaordex  8567  nneob  8585  omsmolem  8586  eldifsucnn  8593  qsss  8715  eroveu  8752  mapsncnv  8834  ralxpmap  8837  elixpsn  8878  ixpsnf1o  8879  boxcutc  8882  pw2f1olem  9012  2pwne  9064  mapxpen  9074  mapunen  9077  php  9134  onomeneq  9141  unxpdomlem2  9160  en1eqsnbi  9179  isfiniteg  9203  fofinf1o  9235  f1opwfi  9259  elfiun  9336  oieu  9447  brwdom2  9481  wdomtr  9483  ixpiunwdom  9498  en3lplem1  9524  suc11reg  9531  inf3lemd  9539  cantnfvalf  9577  cantnflt  9584  cantnfp1lem3  9592  cantnflem2  9602  ttrcltr  9628  rnttrcl  9634  ttrclselem1  9637  r1tr  9691  updjud  9849  dfac8alem  9942  wdomnumr  9977  isinfcard  10005  aceq3lem  10033  dfac5lem4  10039  dfac5lem4OLD  10041  dfac5  10042  dfac2b  10044  coftr  10186  fin23lem28  10253  fin23lem29  10254  fin1a2lem11  10323  fin1a2lem12  10324  fin1a2lem13  10325  hsmexlem9  10338  axdclem  10432  pwcfsdom  10497  gchdomtri  10543  fpwwe2  10557  gchpwdom  10584  gchhar  10593  addnidpi  10815  nqereu  10843  genpv  10913  genpdm  10916  distrlem5pr  10941  mulrid  11133  ltne  11234  mul02  11315  cnegex  11318  mul0or  11781  negfi  12096  sup2  12103  supaddc  12114  supadd  12115  supmul1  12116  supmul  12119  creur  12144  creui  12145  cju  12146  nnsub  12212  un0addcl  12461  un0mulcl  12462  nn0sub  12478  elz2  12533  zaddcl  12558  suprzcl2  12879  qmulz  12892  qre  12894  qnegcl  12907  elpqb  12917  xrmax1  13118  xrmin2  13121  max1ALT  13129  xlesubadd  13206  xmulass  13230  xlemul1a  13231  xrsupexmnf  13248  xrinfmexpnf  13249  xrub  13255  iccid  13334  fzsn  13511  fzsuc2  13527  fz1sbc  13545  elfzp12  13548  modmuladd  13866  seqid3  13999  bcval5  14271  bcpasc  14274  hashbnd  14289  hashnnn0genn0  14296  hashprg  14348  hashfzo  14382  tpfo  14453  wrdl1s1  14568  ccats1alpha  14573  cats1un  14674  s7f1o  14919  shftlem  15021  replim  15069  absmod0  15256  absz  15264  rlimdm  15504  summolem2  15669  summo  15670  zsum  15671  fsum  15673  fsummulc2  15737  fsumconst  15743  fsum00  15752  incexclem  15792  isumsplit  15796  infcvgaux1i  15813  prodmolem2  15891  prodmo  15892  zprod  15893  fprod  15897  prodsn  15918  prodsnf  15920  fprodconst  15934  ruclem2  16190  fzo0dvdseq  16283  bitsf1ocnv  16404  sadcaddlem  16417  smueqlem  16450  gcdabs1  16489  bezoutlem1  16499  bezoutlem3  16501  bezoutlem4  16502  dvdsgcd  16504  dvdsmulgcd  16516  lcmgcdeq  16572  lcmf  16593  lcmfunsnlem1  16597  lcmfunsnlem2lem2  16599  isprm2lem  16641  dvdsprime  16647  isprm5  16668  coprm  16672  prmdvdsexpr  16678  rpexp  16683  phibndlem  16731  dfphi2  16735  hashgcdlem  16749  odzdvds  16757  nnoddn2prm  16773  pythagtriplem1  16778  iserodd  16797  pceulem  16807  pcqmul  16815  pcqcl  16818  pcxnn0cl  16822  pcxcl  16823  pcneg  16836  pcabs  16837  pcgcd1  16839  pcz  16843  pcprmpw2  16844  pcprmpw  16845  dvdsprmpweqle  16848  difsqpwdvds  16849  pcaddlem  16850  pcadd  16851  pcmpt  16854  pockthg  16868  prmreclem5  16882  4sqlem4  16914  mul4sq  16916  vdwapun  16936  vdwlem2  16944  vdwlem6  16948  vdwlem8  16950  vdwlem13  16955  0ram  16982  ram0  16984  ramcl  16991  cshwsiun  17061  wunress  17210  firest  17386  isssc  17778  pospo  18300  latnlej  18413  gsumval2a  18644  xpsmnd0  18737  mnd1id  18739  0subm  18776  mulgnn0p1  19052  mulgnn0ass  19077  cyccom  19169  gicsubgen  19245  symg1bas  19357  snsymgefmndeq  19361  psgnunilem1  19459  psgnunilem2  19461  mndodcongi  19509  oddvdsnn0  19510  odnncl  19511  oddvds  19513  odeq  19516  odeq1  19526  pgpfi2  19572  sylow2a  19585  sylow2blem3  19588  sylow3lem6  19598  lsmelvalm  19617  lsmsubm  19619  lsmsubg  19620  lsmmod  19641  lsmdisj2  19648  efgmnvl  19680  efgtlen  19692  efgs1b  19702  efgrelexlemb  19716  efgredeu  19718  efgcpbllemb  19721  frgpuptinv  19737  frgpup3lem  19743  qusabl  19831  frgpnabllem1  19839  cyggeninv  19849  cyggenod  19850  gsumval3eu  19870  dprdssv  19984  dprdfeq0  19990  dprdsubg  19992  dprddisj2  20007  ablfacrp  20034  pgpfac1lem3  20045  pgpfaclem2  20050  xpsring1d  20304  dvreq1  20382  irredn1  20397  nzrunit  20492  ringcinv  20639  rrgeq0  20668  domneq0  20676  drngmul0orOLD  20729  isabvd  20780  abvdom  20798  issrngd  20823  lmodfopnelem2  20885  lss1d  20949  lspsneq0  20998  lbspss  21069  lsmcl  21070  lvecvs0or  21098  lspindpi  21122  lidl1el  21216  lpiss  21319  lidldvgen  21324  qsssubdrg  21416  zringlpirlem1  21452  pzriprnglem6  21476  pzriprnglem12  21482  znfld  21550  znunit  21553  znrrg  21555  cygznlem3  21559  frgpcyg  21563  psgnghm  21570  ipeq0  21628  cssincl  21678  lsmcss  21682  obselocv  21718  dsmmacl  21731  dsmmlss  21734  mplsubrglem  21992  mplmonmul  22024  mplcoe5lem  22027  mhpsclcl  22123  mhpvarcl  22124  psdmul  22142  coe1tmmul2  22251  coe1tmmul  22252  pf1ind  22330  mat1dimelbas  22446  mdetralt  22583  mdetunilem2  22588  mdetunilem7  22593  mdetunilem9  22595  maducoeval2  22615  chpscmat  22817  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  istopon  22887  eltg3  22937  tgidm  22955  clsval2  23025  opncldf1  23059  restbas  23133  tgrest  23134  restcld  23147  restcldr  23149  restcls  23156  restntr  23157  ordtbas2  23166  ordtbas  23167  ordtrest2lem  23178  ordtrest2  23179  pnfnei  23195  mnfnei  23196  tgcn  23227  cnconst  23259  cnindis  23267  lmss  23273  ordtt1  23354  discmp  23373  1stcrest  23428  2ndcdisj  23431  cldllycmp  23470  txbas  23542  ptpjpre1  23546  ptuni2  23551  ptbasin  23552  ptbasfi  23556  ptopn2  23559  txbasval  23581  ptpjopn  23587  ptclsg  23590  dfac14lem  23592  xkoccn  23594  ptcnp  23597  upxp  23598  ptrescn  23614  txkgen  23627  xkoptsub  23629  xkopt  23630  xkoco1cn  23632  xkoco2cn  23633  xkococn  23635  xkoinjcn  23662  ordthmeolem  23776  ptuncnv  23782  nrmhaus  23801  fbssint  23813  fbfinnfr  23816  fbasrn  23859  isufil2  23883  filufint  23895  rnelfm  23928  fmfnfmlem2  23930  fmfnfmlem3  23931  fmfnfmlem4  23932  fmfnfm  23933  flimtopon  23945  flimclslem  23959  fclstopon  23987  fclscf  24000  flimfnfcls  24003  alexsublem  24019  alexsubALTlem3  24024  alexsubALTlem4  24025  ptcmplem2  24028  tmdgsum2  24071  symgtgp  24081  cldsubg  24086  qustgplem  24096  tgptsmscld  24126  tsmsxplem1  24128  imasdsf1olem  24348  blssps  24399  blss  24400  stdbdxmet  24490  methaus  24495  metrest  24499  nrginvrcn  24667  nmoeq0  24711  blssioo  24770  xrtgioo  24782  xrsxmet  24785  reconnlem1  24802  reconnlem2  24803  xrge0tsms  24810  elcncf1di  24872  iccpnfcnv  24921  evth  24936  lebnumlem1  24938  lebnumlem2  24939  lebnumlem3  24940  nmoleub3  25096  minveclem3b  25405  ivthlem2  25429  ivthlem3  25430  elovolm  25452  ovolmge0  25454  ovoliun  25482  ovolicc2lem3  25496  ovolicc2  25499  voliunlem3  25529  dyaddisj  25573  dyadmax  25575  opnmblALT  25580  ismbfd  25616  ismbf2d  25617  mbfimaopnlem  25632  mbfimaopn2  25634  i1fmullem  25671  i1fres  25682  itg1climres  25691  mbfi1fseqlem4  25695  itg2lcl  25704  itgsplitioo  25815  ellimc2  25854  rolle  25967  dvlip  25970  dvge0  25983  dvne0  25988  lhop1lem  25990  tdeglem4  26035  degltlem1  26047  deg1nn0clb  26065  deg1lt0  26066  dvdsq1p  26138  ply1rem  26141  fta1g  26145  elply2  26171  plyf  26173  ne0p  26182  plyeq0lem  26185  plypf1  26187  0dgrb  26221  coe1termlem  26233  dgrcolem2  26249  plymul0or  26257  plyrem  26282  fta1  26285  quotcan  26286  aalioulem3  26311  eff1olem  26525  lognegb  26567  eflogeq  26579  argregt0  26587  argrege0  26588  tanarg  26596  cxpexp  26645  cxpeq0  26655  mulcxp  26662  cxpeq  26734  atans2  26908  scvxcvx  26963  dmgmaddn0  27000  isppw2  27092  vmappw  27093  vmacl  27095  efvmacl  27097  isnsqf  27112  mumullem2  27157  sqff1o  27159  dvdsppwf1o  27163  ppiublem1  27179  vmalelog  27182  chtublem  27188  fsumvma  27190  perfectlem2  27207  perfect  27208  bposlem1  27261  lgsmod  27300  lgsne0  27312  lgsdirnn0  27321  lgsqr  27328  lgsdchr  27332  gausslemma2dlem1a  27342  gausslemma2dlem6  27349  lgseisenlem2  27353  lgsquadlem1  27357  lgsquadlem2  27358  2lgslem1b  27369  2sqlem2  27395  mul2sq  27396  2sqlem7  27401  dchrisum0fno1  27488  pntrsumbnd2  27544  ostthlem1  27604  ostth2lem2  27611  ostth3  27615  ostth  27616  nolesgn2ores  27650  nogesgn1ores  27652  nolt02o  27673  nogt01o  27674  nosupbnd2  27694  noinfbnd2lem1  27708  noetasuplem4  27714  noetainflem4  27718  maxs1  27747  mins2  27750  ltsne  27752  eqcuts3  27810  cuteq1  27823  madef  27842  ltslpss  27914  lrrecfr  27949  addsval  27968  addsproplem2  27976  addsuniflem  28007  addbdaylem  28023  negsid  28047  negsunif  28061  mulsproplem5  28126  mulsproplem6  28127  mulsproplem7  28128  mulsproplem8  28129  mulsproplem9  28130  lemulsd  28144  sltmuls1  28153  sltmuls2  28154  ltmuls2  28177  muls0ord  28191  precsexlem8  28220  precsexlem9  28221  precsexlem11  28223  elons2  28264  oncutlt  28270  bdayons  28282  onaddscl  28283  onmulscl  28284  nnsge1  28349  n0fincut  28361  n0subs  28369  dfnns2  28378  eucliddivs  28382  znegscl  28398  zaddscl  28400  zmulscld  28403  elzn0s  28404  eln0zs  28406  n0seo  28427  zseo  28428  bdaypw2n0bndlem  28469  bdaypw2n0bnd  28470  z12no  28482  z12addscl  28483  z12negscl  28484  z12shalf  28486  z12zsodd  28488  z12sge0  28489  z12bdaylem  28490  bdayfinlem  28492  recut  28500  elreno2  28501  remulscllem1  28506  colinearalg  28993  axpasch  29024  axlowdimlem16  29040  axlowdimlem17  29041  axlowdim  29044  axcontlem2  29048  axcontlem4  29050  axcontlem7  29053  lpvtx  29151  edglnl  29226  numedglnl  29227  usgredgop  29253  usgrexmplef  29342  uhgrspansubgrlem  29373  uhgrspan1  29386  nbusgredgeu0  29451  nb3grprlem2  29464  cusgrsize2inds  29537  vtxd0nedgb  29572  rusgrpropnb  29667  upgrwlkvtxedg  29728  wlkp1lem1  29755  wlkp1lem6  29760  wlkp1lem8  29762  usgr2wlkneq  29839  crctcshwlk  29905  crctcsh  29907  iswwlksnon  29936  wlkiswwlks1  29950  wwlksnextbi  29977  wwlksnextproplem2  29993  wspthsnonn0vne  30000  clwlkclwwlklem2  30085  clwwisshclwws  30100  erclwwlktr  30107  clwwlkel  30131  clwwlkext2edg  30141  erclwwlkntr  30156  clwlknf1oclwwlknlem2  30167  clwlknf1oclwwlknlem3  30168  clwlknf1oclwwlkn  30169  clwwlknonccat  30181  0wlkons1  30206  3wlkdlem6  30250  eupth2eucrct  30302  frgrwopreglem2  30398  2clwwlk2clwwlk  30435  wlkl0  30452  nvmul0or  30736  ipasslem5  30921  ipasslem11  30926  hvmul0or  31111  his6  31185  hhssnv  31350  ocsh  31369  ocin  31382  shsidmi  31470  chnlen0  31530  h1de2bi  31640  h1de2ctlem  31641  h1de2ci  31642  spansni  31643  3oalem1  31748  nmcexi  32112  atcveq0  32434  chcv1  32441  cdjreui  32518  cdj3lem2b  32523  xrge0tsmsd  33149  1fldgenq  33398  psrmonmul  33709  ccfldextdgrr  33832  ordtrest2NEWlem  34082  ordtrest2NEW  34083  xrge0iifcnv  34093  esumc  34211  esumpcvgval  34238  ballotlemfc0  34653  ballotlemfcc  34654  fissorduni  35249  axprALT2  35269  fineqvnttrclse  35284  gblacfnacd  35300  subfacp1lem4  35381  subfacp1lem5  35382  erdszelem8  35396  sconnpi1  35437  cvmsss2  35472  cvmlift2lem12  35512  satfv0  35556  satfv0fun  35569  satf00  35572  sat1el2xp  35577  fmla0xp  35581  fmlasucdisj  35597  satffunlem1lem1  35600  satffunlem2lem1  35602  dmopab3rexdif  35603  msubco  35729  msubvrs  35758  ellcsrspsn  35839  sinccvglem  35870  untsucf  35908  nnuni  35925  dfrdg2  35991  colineardim1  36259  btwnconn1lem14  36298  segleantisym  36313  colinbtwnle  36316  outsidele  36330  lineunray  36345  linethru  36351  elicc3  36515  opnregcld  36528  cldregopn  36529  fnejoin2  36567  bj-isrvec  37624  dissneqlem  37670  icorempo  37681  relowlssretop  37693  relowlpssretop  37694  rdgssun  37708  finxpsuclem  37727  lindsenlbs  37950  ptrecube  37955  poimirlem6  37961  poimirlem7  37962  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem23  37978  poimirlem24  37979  poimirlem25  37980  poimirlem26  37981  poimirlem27  37982  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  poimirlem32  37987  itg2addnclem3  38008  ftc1anclem6  38033  dvasin  38039  unirep  38049  sdclem2  38077  ssbnd  38123  prdsbnd  38128  cntotbnd  38131  heibor1lem  38144  rrnequiv  38170  ismndo2  38209  grpoeqdivid  38216  isdrngo3  38294  crngohomfo  38341  0idl  38360  1idl  38361  divrngidl  38363  smprngopr  38387  prnc  38402  ispridlc  38405  disjimeceqim  39139  riotaclbgBAD  39414  lshpdisj  39447  lsateln0  39455  lsatcveq0  39492  opnlen0  39648  cmtbr4N  39715  cvrnbtwn2  39735  cvrnbtwn4  39739  atcvreq0  39774  cvlatexch1  39796  exatleN  39864  atlelt  39898  ps-2  39938  llnn0  39976  lplnn0N  40007  islpln2a  40008  lvoln0N  40051  islvol2aN  40052  4at  40073  dalemcea  40120  dalem3  40124  pmapglb2N  40231  pmapglb2xN  40232  cdlema1N  40251  cdlemb  40254  paddasslem17  40296  llnexchb2lem  40328  llnexchb2  40329  lhpat3  40506  ltrnid  40595  trlne  40645  cdlemc4  40654  cdleme11h  40726  cdlemednuN  40760  cdlemg1a  41030  tendoeq2  41234  tendoid0  41285  dva1dim  41445  dib1dim  41625  dihlatat  41797  dochkrshp4  41849  dochkr1  41938  lclkrlem2e  41971  lcfrlem16  42018  lcfrlem28  42030  mapd0  42125  hdmap14lem13  42340  eqresfnbd  42687  f1o2d2  42688  expeq1d  42770  expeqidd  42771  dvdsexpnn0  42780  reladdrsub  42831  sn-remul0ord  42854  sn-negex12  42863  sn-mullid  42882  sn-mul02  42911  nn0addcom  42921  nn0mulcom  42925  zmulcomlem  42926  mulgt0con1d  42929  mulgt0con2d  42930  sn-sup2  42950  frlmsnic  42999  evlselvlem  43033  prjspner1  43073  elrfi  43140  mrefg2  43153  eldiophb  43203  eldioph2b  43209  diophin  43218  diophun  43219  rexzrexnn0  43250  eldioph4b  43257  diophren  43259  rencldnfilem  43266  pellexlem6  43280  jm2.19  43439  rmydioph  43460  expdiophlem1  43467  expdioph  43469  lnr2i  43562  lpirlnr  43563  hbtlem2  43570  hbtlem4  43572  hbtlem6  43575  dgrsub2  43581  dgraa0p  43595  rngunsnply  43615  nlimsuc  43886  dfsucon  43968  radcnvrat  44759  pm14.24  44877  addrcom  44919  modelaxreplem1  45423  ormklocald  47320  natlocalincr  47322  afveu  47613  dfafn5b  47621  rlimdmafv  47637  afv2eu  47698  rlimdmafv2  47718  el1fzopredsuc  47786  minusmod5ne  47815  modmknepk  47828  elsetpreimafvssdm  47858  imasetpreimafvbijlemfo  47877  sprvalpw  47952  prprvalpw  47987  reupr  47994  fmtnofac2lem  48043  proththdlem  48088  perfectALTVlem2  48210  perfectALTV  48211  gbowpos  48247  gbowgt5  48250  gboge9  48252  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  uhgrimedgi  48378  isuspgrim0  48382  isuspgrimlem  48383  upgrimpths  48397  clnbgrgrim  48422  grimedg  48423  grtrissvtx  48432  stgredgiun  48446  stgrvtx0  48450  isubgr3stgrlem7  48460  grlimgrtrilem2  48490  gpgiedgdmellem  48534  gpgvtxel2  48536  gpgvtx0  48541  gpgvtx1  48542  gpgusgralem  48544  gpgedgvtx0  48549  gpgedgvtx1  48550  gpgedg2ov  48554  gpgedg2iv  48555  gpgnbgrvtx0  48562  gpgnbgrvtx1  48563  pgnbgreunbgr  48613  ringcinvALTV  48798  lincellss  48914  lindsrng01  48956  suppdm  48998  nnpw2pb  49075  0aryfvalel  49122  0aryfvalelfv  49123  itsclc0xyqsolr  49257  infsubc  49547  infsubc2  49548