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  4501  elsn2g  4628  preq1b  4810  elpreqprb  4832  reusv3  5360  alxfr  5362  reuhypd  5374  axpr  5382  opth1  5435  euotd  5473  otiunsndisj  5480  tz7.2  5621  frsn  5726  dmopab2rex  5881  elsnxp  6264  reuop  6266  dfpo2  6269  ordtri1  6365  ordtri3  6368  fvmptdv2  6986  fveqressseq  7051  foco2  7081  fsn  7107  fnsnbg  7138  fnsnbOLD  7140  fmptsng  7142  fmptsnd  7143  fconst2g  7177  fnprb  7182  fntpb  7183  funfvima  7204  soisoi  7303  isores3  7310  eqfunresadj  7335  riotaeqimp  7370  eusvobj2  7379  ovmpodv2  7547  f1opw2  7644  sorpssun  7706  sorpssin  7707  oneqmin  7776  nlimsucg  7818  onzsl  7822  tfinds  7836  funcnvuni  7908  mptcnfimad  7965  opiota  8038  mposn  8082  frpoins3xpg  8119  frpoins3xp3g  8120  poxp2  8122  xpord2pred  8124  sexp2  8125  poxp3  8129  xpord3pred  8131  sexp3  8132  xpord3inddlem  8133  suppssov1  8176  suppssov2  8177  suppssfv  8181  brtpos  8214  frrlem12  8276  frrlem13  8277  seqomlem1  8418  seqomlem2  8419  omordi  8530  omord  8532  omwordi  8535  oeeui  8566  nnmordi  8595  nnmord  8596  nnmwordi  8599  nnawordex  8601  nnaordex  8602  nneob  8620  omsmolem  8621  eldifsucnn  8628  qsss  8749  eroveu  8785  mapsncnv  8866  ralxpmap  8869  elixpsn  8910  ixpsnf1o  8911  boxcutc  8914  pw2f1olem  9045  2pwne  9097  mapxpen  9107  mapunen  9110  php  9171  onomeneq  9178  unxpdomlem2  9198  en1eqsnbi  9221  isfiniteg  9248  fofinf1o  9283  f1opwfi  9307  elfiun  9381  oieu  9492  brwdom2  9526  wdomtr  9528  ixpiunwdom  9543  en3lplem1  9565  suc11reg  9572  inf3lemd  9580  cantnfvalf  9618  cantnflt  9625  cantnfp1lem3  9633  cantnflem2  9643  ttrcltr  9669  rnttrcl  9675  ttrclselem1  9678  r1tr  9729  updjud  9887  dfac8alem  9982  wdomnumr  10017  isinfcard  10045  aceq3lem  10073  dfac5lem4  10079  dfac5lem4OLD  10081  dfac5  10082  dfac2b  10084  coftr  10226  fin23lem28  10293  fin23lem29  10294  fin1a2lem11  10363  fin1a2lem12  10364  fin1a2lem13  10365  hsmexlem9  10378  axdclem  10472  pwcfsdom  10536  gchdomtri  10582  fpwwe2  10596  gchpwdom  10623  gchhar  10632  addnidpi  10854  nqereu  10882  genpv  10952  genpdm  10955  distrlem5pr  10980  mulrid  11172  ltne  11271  mul02  11352  cnegex  11355  mul0or  11818  negfi  12132  sup2  12139  supaddc  12150  supadd  12151  supmul1  12152  supmul  12155  creur  12180  creui  12181  cju  12182  nnsub  12230  un0addcl  12475  un0mulcl  12476  nn0sub  12492  elz2  12547  zaddcl  12573  suprzcl2  12897  qmulz  12910  qre  12912  qnegcl  12925  elpqb  12935  xrmax1  13135  xrmin2  13138  max1ALT  13146  xlesubadd  13223  xmulass  13247  xlemul1a  13248  xrsupexmnf  13265  xrinfmexpnf  13266  xrub  13272  iccid  13351  fzsn  13527  fzsuc2  13543  fz1sbc  13561  elfzp12  13564  modmuladd  13878  seqid3  14011  bcval5  14283  bcpasc  14286  hashbnd  14301  hashnnn0genn0  14308  hashprg  14360  hashfzo  14394  tpfo  14465  wrdl1s1  14579  ccats1alpha  14584  cats1un  14686  s7f1o  14932  shftlem  15034  replim  15082  absmod0  15269  absz  15277  rlimdm  15517  summolem2  15682  summo  15683  zsum  15684  fsum  15686  fsummulc2  15750  fsumconst  15756  fsum00  15764  incexclem  15802  isumsplit  15806  infcvgaux1i  15823  prodmolem2  15901  prodmo  15902  zprod  15903  fprod  15907  prodsn  15928  prodsnf  15930  fprodconst  15944  ruclem2  16200  fzo0dvdseq  16293  bitsf1ocnv  16414  sadcaddlem  16427  smueqlem  16460  gcdabs1  16499  bezoutlem1  16509  bezoutlem3  16511  bezoutlem4  16512  dvdsgcd  16514  dvdsmulgcd  16526  lcmgcdeq  16582  lcmf  16603  lcmfunsnlem1  16607  lcmfunsnlem2lem2  16609  isprm2lem  16651  dvdsprime  16657  isprm5  16677  coprm  16681  prmdvdsexpr  16687  rpexp  16692  phibndlem  16740  dfphi2  16744  hashgcdlem  16758  odzdvds  16766  nnoddn2prm  16782  pythagtriplem1  16787  iserodd  16806  pceulem  16816  pcqmul  16824  pcqcl  16827  pcxnn0cl  16831  pcxcl  16832  pcneg  16845  pcabs  16846  pcgcd1  16848  pcz  16852  pcprmpw2  16853  pcprmpw  16854  dvdsprmpweqle  16857  difsqpwdvds  16858  pcaddlem  16859  pcadd  16860  pcmpt  16863  pockthg  16877  prmreclem5  16891  4sqlem4  16923  mul4sq  16925  vdwapun  16945  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  vdwlem13  16964  0ram  16991  ram0  16993  ramcl  17000  cshwsiun  17070  wunress  17219  firest  17395  isssc  17782  pospo  18304  latnlej  18415  gsumval2a  18612  xpsmnd0  18705  mnd1id  18707  0subm  18744  mulgnn0p1  19017  mulgnn0ass  19042  cyccom  19135  gicsubgen  19211  symg1bas  19321  snsymgefmndeq  19325  psgnunilem1  19423  psgnunilem2  19425  mndodcongi  19473  oddvdsnn0  19474  odnncl  19475  oddvds  19477  odeq  19480  odeq1  19490  pgpfi2  19536  sylow2a  19549  sylow2blem3  19552  sylow3lem6  19562  lsmelvalm  19581  lsmsubm  19583  lsmsubg  19584  lsmmod  19605  lsmdisj2  19612  efgmnvl  19644  efgtlen  19656  efgs1b  19666  efgrelexlemb  19680  efgredeu  19682  efgcpbllemb  19685  frgpuptinv  19701  frgpup3lem  19707  qusabl  19795  frgpnabllem1  19803  cyggeninv  19813  cyggenod  19814  gsumval3eu  19834  dprdssv  19948  dprdfeq0  19954  dprdsubg  19956  dprddisj2  19971  ablfacrp  19998  pgpfac1lem3  20009  pgpfaclem2  20014  xpsring1d  20242  dvreq1  20320  irredn1  20335  nzrunit  20433  ringcinv  20580  rrgeq0  20609  domneq0  20617  drngmul0orOLD  20670  isabvd  20721  abvdom  20739  issrngd  20764  lmodfopnelem2  20805  lss1d  20869  lspsneq0  20918  lbspss  20989  lsmcl  20990  lvecvs0or  21018  lspindpi  21042  lidl1el  21136  lpiss  21239  lidldvgen  21244  qsssubdrg  21343  zringlpirlem1  21372  pzriprnglem6  21396  pzriprnglem12  21402  znfld  21470  znunit  21473  znrrg  21475  cygznlem3  21479  frgpcyg  21483  psgnghm  21489  ipeq0  21547  cssincl  21597  lsmcss  21601  obselocv  21637  dsmmacl  21650  dsmmlss  21653  mplsubrglem  21913  mplmonmul  21943  mplcoe5lem  21946  mhpsclcl  22034  mhpvarcl  22035  psdmul  22053  coe1tmmul2  22162  coe1tmmul  22163  pf1ind  22242  mat1dimelbas  22358  mdetralt  22495  mdetunilem2  22500  mdetunilem7  22505  mdetunilem9  22507  maducoeval2  22527  chpscmat  22729  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  istopon  22799  eltg3  22849  tgidm  22867  clsval2  22937  opncldf1  22971  restbas  23045  tgrest  23046  restcld  23059  restcldr  23061  restcls  23068  restntr  23069  ordtbas2  23078  ordtbas  23079  ordtrest2lem  23090  ordtrest2  23091  pnfnei  23107  mnfnei  23108  tgcn  23139  cnconst  23171  cnindis  23179  lmss  23185  ordtt1  23266  discmp  23285  1stcrest  23340  2ndcdisj  23343  cldllycmp  23382  txbas  23454  ptpjpre1  23458  ptuni2  23463  ptbasin  23464  ptbasfi  23468  ptopn2  23471  txbasval  23493  ptpjopn  23499  ptclsg  23502  dfac14lem  23504  xkoccn  23506  ptcnp  23509  upxp  23510  ptrescn  23526  txkgen  23539  xkoptsub  23541  xkopt  23542  xkoco1cn  23544  xkoco2cn  23545  xkococn  23547  xkoinjcn  23574  ordthmeolem  23688  ptuncnv  23694  nrmhaus  23713  fbssint  23725  fbfinnfr  23728  fbasrn  23771  isufil2  23795  filufint  23807  rnelfm  23840  fmfnfmlem2  23842  fmfnfmlem3  23843  fmfnfmlem4  23844  fmfnfm  23845  flimtopon  23857  flimclslem  23871  fclstopon  23899  fclscf  23912  flimfnfcls  23915  alexsublem  23931  alexsubALTlem3  23936  alexsubALTlem4  23937  ptcmplem2  23940  tmdgsum2  23983  symgtgp  23993  cldsubg  23998  qustgplem  24008  tgptsmscld  24038  tsmsxplem1  24040  imasdsf1olem  24261  blssps  24312  blss  24313  stdbdxmet  24403  methaus  24408  metrest  24412  nrginvrcn  24580  nmoeq0  24624  blssioo  24683  xrtgioo  24695  xrsxmet  24698  reconnlem1  24715  reconnlem2  24716  xrge0tsms  24723  elcncf1di  24788  iccpnfcnv  24842  evth  24858  lebnumlem1  24860  lebnumlem2  24861  lebnumlem3  24862  nmoleub3  25019  minveclem3b  25328  ivthlem2  25353  ivthlem3  25354  elovolm  25376  ovolmge0  25378  ovoliun  25406  ovolicc2lem3  25420  ovolicc2  25423  voliunlem3  25453  dyaddisj  25497  dyadmax  25499  opnmblALT  25504  ismbfd  25540  ismbf2d  25541  mbfimaopnlem  25556  mbfimaopn2  25558  i1fmullem  25595  i1fres  25606  itg1climres  25615  mbfi1fseqlem4  25619  itg2lcl  25628  itgsplitioo  25739  ellimc2  25778  rolle  25894  dvlip  25898  dvge0  25911  dvne0  25916  lhop1lem  25918  tdeglem4  25965  degltlem1  25977  deg1nn0clb  25995  deg1lt0  25996  dvdsq1p  26068  ply1rem  26071  fta1g  26075  elply2  26101  plyf  26103  ne0p  26112  plyeq0lem  26115  plypf1  26117  0dgrb  26151  coe1termlem  26163  dgrcolem2  26180  plymul0or  26188  plyrem  26213  fta1  26216  quotcan  26217  aalioulem3  26242  eff1olem  26457  lognegb  26499  eflogeq  26511  argregt0  26519  argrege0  26520  tanarg  26528  cxpexp  26577  cxpeq0  26587  mulcxp  26594  cxpeq  26667  atans2  26841  scvxcvx  26896  dmgmaddn0  26933  isppw2  27025  vmappw  27026  vmacl  27028  efvmacl  27030  isnsqf  27045  mumullem2  27090  sqff1o  27092  dvdsppwf1o  27096  ppiublem1  27113  vmalelog  27116  chtublem  27122  fsumvma  27124  perfectlem2  27141  perfect  27142  bposlem1  27195  lgsmod  27234  lgsne0  27246  lgsdirnn0  27255  lgsqr  27262  lgsdchr  27266  gausslemma2dlem1a  27276  gausslemma2dlem6  27283  lgseisenlem2  27287  lgsquadlem1  27291  lgsquadlem2  27292  2lgslem1b  27303  2sqlem2  27329  mul2sq  27330  2sqlem7  27335  dchrisum0fno1  27422  pntrsumbnd2  27478  ostthlem1  27538  ostth2lem2  27545  ostth3  27549  ostth  27550  nolesgn2ores  27584  nogesgn1ores  27586  nolt02o  27607  nogt01o  27608  nosupbnd2  27628  noinfbnd2lem1  27642  noetasuplem4  27648  noetainflem4  27652  maxs1  27677  mins2  27680  sltne  27682  ssltsn  27704  cuteq1  27746  madef  27764  sltlpss  27819  lrrecfr  27850  addsval  27869  addsproplem2  27877  addsuniflem  27908  addsbdaylem  27923  negsid  27947  negsunif  27961  mulsproplem5  28023  mulsproplem6  28024  mulsproplem7  28025  mulsproplem8  28026  mulsproplem9  28027  slemuld  28041  ssltmul1  28050  ssltmul2  28051  sltmul2  28074  muls0ord  28088  precsexlem8  28116  precsexlem9  28117  precsexlem11  28119  elons2  28159  onscutlt  28165  bdayon  28173  onaddscl  28174  onmulscl  28175  nnsge1  28235  n0sfincut  28246  n0subs  28253  dfnns2  28261  eucliddivs  28265  znegscl  28280  zaddscl  28282  zmulscld  28285  elzn0s  28286  eln0zs  28288  n0seo  28307  zseo  28308  zs12negscl  28340  zs12ge0  28342  zs12bday  28343  recut  28347  0reno  28348  remulscllem1  28351  colinearalg  28837  axpasch  28868  axlowdimlem16  28884  axlowdimlem17  28885  axlowdim  28888  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  lpvtx  28995  edglnl  29070  numedglnl  29071  usgredgop  29097  usgrexmplef  29186  uhgrspansubgrlem  29217  uhgrspan1  29230  nbusgredgeu0  29295  nb3grprlem2  29308  cusgrsize2inds  29381  vtxd0nedgb  29416  rusgrpropnb  29511  upgrwlkvtxedg  29573  wlkp1lem1  29601  wlkp1lem6  29606  wlkp1lem8  29608  usgr2wlkneq  29686  crctcshwlk  29752  crctcsh  29754  iswwlksnon  29783  wlkiswwlks1  29797  wwlksnextbi  29824  wwlksnextproplem2  29840  wspthsnonn0vne  29847  clwlkclwwlklem2  29929  clwwisshclwws  29944  erclwwlktr  29951  clwwlkel  29975  clwwlkext2edg  29985  erclwwlkntr  30000  clwlknf1oclwwlknlem2  30011  clwlknf1oclwwlknlem3  30012  clwlknf1oclwwlkn  30013  clwwlknonccat  30025  0wlkons1  30050  3wlkdlem6  30094  eupth2eucrct  30146  frgrwopreglem2  30242  2clwwlk2clwwlk  30279  wlkl0  30296  nvmul0or  30579  ipasslem5  30764  ipasslem11  30769  hvmul0or  30954  his6  31028  hhssnv  31193  ocsh  31212  ocin  31225  shsidmi  31313  chnlen0  31373  h1de2bi  31483  h1de2ctlem  31484  h1de2ci  31485  spansni  31486  3oalem1  31591  nmcexi  31955  atcveq0  32277  chcv1  32284  cdjreui  32361  cdj3lem2b  32366  xrge0tsmsd  33002  1fldgenq  33272  ccfldextdgrr  33667  ordtrest2NEWlem  33912  ordtrest2NEW  33913  xrge0iifcnv  33923  esumc  34041  esumpcvgval  34068  ballotlemfc0  34484  ballotlemfcc  34485  gblacfnacd  35089  subfacp1lem4  35170  subfacp1lem5  35171  erdszelem8  35185  sconnpi1  35226  cvmsss2  35261  cvmlift2lem12  35301  satfv0  35345  satfv0fun  35358  satf00  35361  sat1el2xp  35366  fmla0xp  35370  fmlasucdisj  35386  satffunlem1lem1  35389  satffunlem2lem1  35391  dmopab3rexdif  35392  msubco  35518  msubvrs  35547  ellcsrspsn  35628  sinccvglem  35659  untsucf  35697  nnuni  35714  dfrdg2  35783  colineardim1  36049  btwnconn1lem14  36088  segleantisym  36103  colinbtwnle  36106  outsidele  36120  lineunray  36135  linethru  36141  elicc3  36305  opnregcld  36318  cldregopn  36319  fnejoin2  36357  bj-isrvec  37282  dissneqlem  37328  icorempo  37339  relowlssretop  37351  relowlpssretop  37352  rdgssun  37366  finxpsuclem  37385  lindsenlbs  37609  ptrecube  37614  poimirlem6  37620  poimirlem7  37621  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  itg2addnclem3  37667  ftc1anclem6  37692  dvasin  37698  unirep  37708  sdclem2  37736  ssbnd  37782  prdsbnd  37787  cntotbnd  37790  heibor1lem  37803  rrnequiv  37829  ismndo2  37868  grpoeqdivid  37875  isdrngo3  37953  crngohomfo  38000  0idl  38019  1idl  38020  divrngidl  38022  smprngopr  38046  prnc  38061  ispridlc  38064  riotaclbgBAD  38947  lshpdisj  38980  lsateln0  38988  lsatcveq0  39025  opnlen0  39181  cmtbr4N  39248  cvrnbtwn2  39268  cvrnbtwn4  39272  atcvreq0  39307  cvlatexch1  39329  exatleN  39398  atlelt  39432  ps-2  39472  llnn0  39510  lplnn0N  39541  islpln2a  39542  lvoln0N  39585  islvol2aN  39586  4at  39607  dalemcea  39654  dalem3  39658  pmapglb2N  39765  pmapglb2xN  39766  cdlema1N  39785  cdlemb  39788  paddasslem17  39830  llnexchb2lem  39862  llnexchb2  39863  lhpat3  40040  ltrnid  40129  trlne  40179  cdlemc4  40188  cdleme11h  40260  cdlemednuN  40294  cdlemg1a  40564  tendoeq2  40768  tendoid0  40819  dva1dim  40979  dib1dim  41159  dihlatat  41331  dochkrshp4  41383  dochkr1  41472  lclkrlem2e  41505  lcfrlem16  41552  lcfrlem28  41564  mapd0  41659  hdmap14lem13  41874  eqresfnbd  42220  f1o2d2  42221  expeq1d  42312  expeqidd  42313  dvdsexpnn0  42322  reladdrsub  42373  sn-remul0ord  42396  sn-negex12  42405  sn-mullid  42424  sn-mul02  42440  nn0addcom  42450  nn0mulcom  42454  zmulcomlem  42455  mulgt0con1d  42458  mulgt0con2d  42459  sn-sup2  42479  frlmsnic  42528  evlselvlem  42574  prjspner1  42614  elrfi  42682  mrefg2  42695  eldiophb  42745  eldioph2b  42751  diophin  42760  diophun  42761  rexzrexnn0  42792  eldioph4b  42799  diophren  42801  rencldnfilem  42808  pellexlem6  42822  jm2.19  42982  rmydioph  43003  expdiophlem1  43010  expdioph  43012  lnr2i  43105  lpirlnr  43106  hbtlem2  43113  hbtlem4  43115  hbtlem6  43118  dgrsub2  43124  dgraa0p  43138  rngunsnply  43158  nlimsuc  43430  dfsucon  43512  radcnvrat  44303  pm14.24  44421  addrcom  44464  modelaxreplem1  44968  ormklocald  46872  natlocalincr  46874  afveu  47154  dfafn5b  47162  rlimdmafv  47178  afv2eu  47239  rlimdmafv2  47259  el1fzopredsuc  47326  minusmod5ne  47350  modmknepk  47363  elsetpreimafvssdm  47387  imasetpreimafvbijlemfo  47406  sprvalpw  47481  prprvalpw  47516  reupr  47523  fmtnofac2lem  47569  proththdlem  47614  perfectALTVlem2  47723  perfectALTV  47724  gbowpos  47760  gbowgt5  47763  gboge9  47765  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  uhgrimedgi  47890  isuspgrim0  47894  isuspgrimlem  47895  upgrimpths  47909  clnbgrgrim  47934  grimedg  47935  grtrissvtx  47943  stgredgiun  47957  stgrvtx0  47961  isubgr3stgrlem7  47971  grlimgrtrilem2  47994  gpgiedgdmellem  48037  gpgvtxel2  48039  gpgvtx0  48044  gpgvtx1  48045  gpgusgralem  48047  gpgedgvtx0  48052  gpgedgvtx1  48053  gpgedg2ov  48057  gpgedg2iv  48058  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  pgnbgreunbgr  48115  ringcinvALTV  48298  lincellss  48415  lindsrng01  48457  suppdm  48499  nnpw2pb  48576  0aryfvalel  48623  0aryfvalelfv  48624  itsclc0xyqsolr  48758  infsubc  49049  infsubc2  49050