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  elsn2g  4686  preq1b  4871  elpreqprb  4892  reusv3  5423  alxfr  5425  reuhypd  5437  opth1  5495  euotd  5532  otiunsndisj  5539  tz7.2  5683  frsn  5787  dmopab2rex  5942  elsnxp  6322  reuop  6324  dfpo2  6327  ordtri1  6428  ordtri3  6431  fvmptdv2  7047  fveqressseq  7113  foco2  7143  fsn  7169  fnsnb  7200  fmptsng  7202  fmptsnd  7203  fconst2g  7240  fnprb  7245  fntpb  7246  funfvima  7267  soisoi  7364  isores3  7371  eqfunresadj  7396  riotaeqimp  7431  eusvobj2  7440  ovmpodv2  7608  f1opw2  7705  sorpssun  7765  sorpssin  7766  oneqmin  7836  nlimsucg  7879  onzsl  7883  tfinds  7897  funcnvuni  7972  mptcnfimad  8027  opiota  8100  mposn  8144  frpoins3xpg  8181  frpoins3xp3g  8182  poxp2  8184  xpord2pred  8186  sexp2  8187  poxp3  8191  xpord3pred  8193  sexp3  8194  xpord3inddlem  8195  suppssov1  8238  suppssov2  8239  suppssfv  8243  brtpos  8276  frrlem12  8338  frrlem13  8339  wfrlem10OLD  8374  wfrlem14OLD  8378  wfrlem15OLD  8379  seqomlem1  8506  seqomlem2  8507  omordi  8622  omord  8624  omwordi  8627  oeeui  8658  nnmordi  8687  nnmord  8688  nnmwordi  8691  nnawordex  8693  nnaordex  8694  nneob  8712  omsmolem  8713  eldifsucnn  8720  qsss  8836  eroveu  8870  mapsncnv  8951  ralxpmap  8954  elixpsn  8995  ixpsnf1o  8996  boxcutc  8999  pw2f1olem  9142  2pwne  9199  mapxpen  9209  mapunen  9212  php  9273  phpOLD  9285  onomeneq  9291  unxpdomlem2  9314  en1eqsnbi  9338  isfiniteg  9365  fofinf1o  9400  f1opwfi  9426  elfiun  9499  oieu  9608  brwdom2  9642  wdomtr  9644  ixpiunwdom  9659  en3lplem1  9681  suc11reg  9688  inf3lemd  9696  cantnfvalf  9734  cantnflt  9741  cantnfp1lem3  9749  cantnflem2  9759  ttrcltr  9785  rnttrcl  9791  ttrclselem1  9794  r1tr  9845  updjud  10003  dfac8alem  10098  wdomnumr  10133  isinfcard  10161  aceq3lem  10189  dfac5lem4  10195  dfac5lem4OLD  10197  dfac5  10198  dfac2b  10200  coftr  10342  fin23lem28  10409  fin23lem29  10410  fin1a2lem11  10479  fin1a2lem12  10480  fin1a2lem13  10481  hsmexlem9  10494  axdclem  10588  pwcfsdom  10652  gchdomtri  10698  fpwwe2  10712  gchpwdom  10739  gchhar  10748  addnidpi  10970  nqereu  10998  genpv  11068  genpdm  11071  distrlem5pr  11096  mulrid  11288  ltne  11387  mul02  11468  cnegex  11471  mul0or  11930  negfi  12244  sup2  12251  supaddc  12262  supadd  12263  supmul1  12264  supmul  12267  creur  12287  creui  12288  cju  12289  nnsub  12337  un0addcl  12586  un0mulcl  12587  nn0sub  12603  elz2  12657  zaddcl  12683  suprzcl2  13003  qmulz  13016  qre  13018  qnegcl  13031  elpqb  13041  xrmax1  13237  xrmin2  13240  max1ALT  13248  xlesubadd  13325  xmulass  13349  xlemul1a  13350  xrsupexmnf  13367  xrinfmexpnf  13368  xrub  13374  iccid  13452  fzsn  13626  fzsuc2  13642  fz1sbc  13660  elfzp12  13663  modmuladd  13964  seqid3  14097  bcval5  14367  bcpasc  14370  hashbnd  14385  hashnnn0genn0  14392  hashprg  14444  hashfzo  14478  tpfo  14549  wrdl1s1  14662  ccats1alpha  14667  cats1un  14769  s7f1o  15015  shftlem  15117  replim  15165  absmod0  15352  absz  15360  rlimdm  15597  summolem2  15764  summo  15765  zsum  15766  fsum  15768  fsummulc2  15832  fsumconst  15838  fsum00  15846  incexclem  15884  isumsplit  15888  infcvgaux1i  15905  prodmolem2  15983  prodmo  15984  zprod  15985  fprod  15989  prodsn  16010  prodsnf  16012  fprodconst  16026  ruclem2  16280  fzo0dvdseq  16371  bitsf1ocnv  16490  sadcaddlem  16503  smueqlem  16536  gcdabs1  16575  bezoutlem1  16586  bezoutlem3  16588  bezoutlem4  16589  dvdsgcd  16591  dvdsmulgcd  16603  lcmgcdeq  16659  lcmf  16680  lcmfunsnlem1  16684  lcmfunsnlem2lem2  16686  isprm2lem  16728  dvdsprime  16734  isprm5  16754  coprm  16758  prmdvdsexpr  16764  rpexp  16769  phibndlem  16817  dfphi2  16821  hashgcdlem  16835  odzdvds  16842  nnoddn2prm  16858  pythagtriplem1  16863  iserodd  16882  pceulem  16892  pcqmul  16900  pcqcl  16903  pcxnn0cl  16907  pcxcl  16908  pcneg  16921  pcabs  16922  pcgcd1  16924  pcz  16928  pcprmpw2  16929  pcprmpw  16930  dvdsprmpweqle  16933  difsqpwdvds  16934  pcaddlem  16935  pcadd  16936  pcmpt  16939  pockthg  16953  prmreclem5  16967  4sqlem4  16999  mul4sq  17001  vdwapun  17021  vdwlem2  17029  vdwlem6  17033  vdwlem8  17035  vdwlem13  17040  0ram  17067  ram0  17069  ramcl  17076  cshwsiun  17147  wunress  17309  wunressOLD  17310  firest  17492  isssc  17881  pospo  18415  latnlej  18526  gsumval2a  18723  xpsmnd0  18813  mnd1id  18815  0subm  18852  mulgnn0p1  19125  mulgnn0ass  19150  cyccom  19243  gicsubgen  19319  symg1bas  19432  snsymgefmndeq  19436  psgnunilem1  19535  psgnunilem2  19537  mndodcongi  19585  oddvdsnn0  19586  odnncl  19587  oddvds  19589  odeq  19592  odeq1  19602  pgpfi2  19648  sylow2a  19661  sylow2blem3  19664  sylow3lem6  19674  lsmelvalm  19693  lsmsubm  19695  lsmsubg  19696  lsmmod  19717  lsmdisj2  19724  efgmnvl  19756  efgtlen  19768  efgs1b  19778  efgrelexlemb  19792  efgredeu  19794  efgcpbllemb  19797  frgpuptinv  19813  frgpup3lem  19819  qusabl  19907  frgpnabllem1  19915  cyggeninv  19925  cyggenod  19926  gsumval3eu  19946  dprdssv  20060  dprdfeq0  20066  dprdsubg  20068  dprddisj2  20083  ablfacrp  20110  pgpfac1lem3  20121  pgpfaclem2  20126  xpsring1d  20356  dvreq1  20437  irredn1  20452  nzrunit  20550  ringcinv  20693  rrgeq0  20722  domneq0  20730  drngmul0orOLD  20783  isabvd  20835  abvdom  20853  issrngd  20878  lmodfopnelem2  20919  lss1d  20984  lspsneq0  21033  lbspss  21104  lsmcl  21105  lvecvs0or  21133  lspindpi  21157  lidl1el  21259  lpiss  21362  lidldvgen  21367  qsssubdrg  21467  zringlpirlem1  21496  pzriprnglem6  21520  pzriprnglem12  21526  znfld  21602  znunit  21605  znrrg  21607  cygznlem3  21611  frgpcyg  21615  psgnghm  21621  ipeq0  21679  cssincl  21729  lsmcss  21733  obselocv  21771  dsmmacl  21784  dsmmlss  21787  mplsubrglem  22047  mplmonmul  22077  mplcoe5lem  22080  mhpsclcl  22174  mhpvarcl  22175  psdmul  22193  coe1tmmul2  22300  coe1tmmul  22301  pf1ind  22380  mat1dimelbas  22498  mdetralt  22635  mdetunilem2  22640  mdetunilem7  22645  mdetunilem9  22647  maducoeval2  22667  chpscmat  22869  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  istopon  22939  eltg3  22990  tgidm  23008  clsval2  23079  opncldf1  23113  restbas  23187  tgrest  23188  restcld  23201  restcldr  23203  restcls  23210  restntr  23211  ordtbas2  23220  ordtbas  23221  ordtrest2lem  23232  ordtrest2  23233  pnfnei  23249  mnfnei  23250  tgcn  23281  cnconst  23313  cnindis  23321  lmss  23327  ordtt1  23408  discmp  23427  1stcrest  23482  2ndcdisj  23485  cldllycmp  23524  txbas  23596  ptpjpre1  23600  ptuni2  23605  ptbasin  23606  ptbasfi  23610  ptopn2  23613  txbasval  23635  ptpjopn  23641  ptclsg  23644  dfac14lem  23646  xkoccn  23648  ptcnp  23651  upxp  23652  ptrescn  23668  txkgen  23681  xkoptsub  23683  xkopt  23684  xkoco1cn  23686  xkoco2cn  23687  xkococn  23689  xkoinjcn  23716  ordthmeolem  23830  ptuncnv  23836  nrmhaus  23855  fbssint  23867  fbfinnfr  23870  fbasrn  23913  isufil2  23937  filufint  23949  rnelfm  23982  fmfnfmlem2  23984  fmfnfmlem3  23985  fmfnfmlem4  23986  fmfnfm  23987  flimtopon  23999  flimclslem  24013  fclstopon  24041  fclscf  24054  flimfnfcls  24057  alexsublem  24073  alexsubALTlem3  24078  alexsubALTlem4  24079  ptcmplem2  24082  tmdgsum2  24125  symgtgp  24135  cldsubg  24140  qustgplem  24150  tgptsmscld  24180  tsmsxplem1  24182  imasdsf1olem  24404  blssps  24455  blss  24456  stdbdxmet  24549  methaus  24554  metrest  24558  nrginvrcn  24734  nmoeq0  24778  blssioo  24836  xrtgioo  24847  xrsxmet  24850  reconnlem1  24867  reconnlem2  24868  xrge0tsms  24875  elcncf1di  24940  iccpnfcnv  24994  evth  25010  lebnumlem1  25012  lebnumlem2  25013  lebnumlem3  25014  nmoleub3  25171  minveclem3b  25481  ivthlem2  25506  ivthlem3  25507  elovolm  25529  ovolmge0  25531  ovoliun  25559  ovolicc2lem3  25573  ovolicc2  25576  voliunlem3  25606  dyaddisj  25650  dyadmax  25652  opnmblALT  25657  ismbfd  25693  ismbf2d  25694  mbfimaopnlem  25709  mbfimaopn2  25711  i1fmullem  25748  i1fres  25760  itg1climres  25769  mbfi1fseqlem4  25773  itg2lcl  25782  itgsplitioo  25893  ellimc2  25932  rolle  26048  dvlip  26052  dvge0  26065  dvne0  26070  lhop1lem  26072  tdeglem4  26119  degltlem1  26131  deg1nn0clb  26149  deg1lt0  26150  dvdsq1p  26222  ply1rem  26225  fta1g  26229  elply2  26255  plyf  26257  ne0p  26266  plyeq0lem  26269  plypf1  26271  0dgrb  26305  coe1termlem  26317  dgrcolem2  26334  plymul0or  26340  plyrem  26365  fta1  26368  quotcan  26369  aalioulem3  26394  eff1olem  26608  lognegb  26650  eflogeq  26662  argregt0  26670  argrege0  26671  tanarg  26679  cxpexp  26728  cxpeq0  26738  mulcxp  26745  cxpeq  26818  atans2  26992  scvxcvx  27047  dmgmaddn0  27084  isppw2  27176  vmappw  27177  vmacl  27179  efvmacl  27181  isnsqf  27196  mumullem2  27241  sqff1o  27243  dvdsppwf1o  27247  ppiublem1  27264  vmalelog  27267  chtublem  27273  fsumvma  27275  perfectlem2  27292  perfect  27293  bposlem1  27346  lgsmod  27385  lgsne0  27397  lgsdirnn0  27406  lgsqr  27413  lgsdchr  27417  gausslemma2dlem1a  27427  gausslemma2dlem6  27434  lgseisenlem2  27438  lgsquadlem1  27442  lgsquadlem2  27443  2lgslem1b  27454  2sqlem2  27480  mul2sq  27481  2sqlem7  27486  dchrisum0fno1  27573  pntrsumbnd2  27629  ostthlem1  27689  ostth2lem2  27696  ostth3  27700  ostth  27701  nolesgn2ores  27735  nogesgn1ores  27737  nolt02o  27758  nogt01o  27759  nosupbnd2  27779  noinfbnd2lem1  27793  noetasuplem4  27799  noetainflem4  27803  maxs1  27828  mins2  27831  sltne  27833  ssltsn  27855  cuteq1  27896  madef  27913  sltlpss  27963  lrrecfr  27994  addsval  28013  addsproplem2  28021  addsuniflem  28052  addsbdaylem  28067  negsid  28091  negsunif  28105  mulsproplem5  28164  mulsproplem6  28165  mulsproplem7  28166  mulsproplem8  28167  mulsproplem9  28168  slemuld  28182  ssltmul1  28191  ssltmul2  28192  sltmul2  28215  muls0ord  28229  precsexlem8  28256  precsexlem9  28257  precsexlem11  28259  elons2  28299  onaddscl  28304  onmulscl  28305  nnsge1  28364  n0subs  28378  dfnns2  28380  znegscl  28396  zaddscl  28398  zmulscld  28401  elzn0s  28402  eln0zs  28404  n0seo  28423  zseo  28424  zs12bday  28442  recut  28446  0reno  28447  remulscllem1  28450  colinearalg  28943  axpasch  28974  axlowdimlem16  28990  axlowdimlem17  28991  axlowdim  28994  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  lpvtx  29103  edglnl  29178  numedglnl  29179  usgredgop  29205  usgrexmplef  29294  uhgrspansubgrlem  29325  uhgrspan1  29338  nbusgredgeu0  29403  nb3grprlem2  29416  cusgrsize2inds  29489  vtxd0nedgb  29524  rusgrpropnb  29619  upgrwlkvtxedg  29681  wlkp1lem1  29709  wlkp1lem6  29714  wlkp1lem8  29716  usgr2wlkneq  29792  crctcshwlk  29855  crctcsh  29857  iswwlksnon  29886  wlkiswwlks1  29900  wwlksnextbi  29927  wwlksnextproplem2  29943  wspthsnonn0vne  29950  clwlkclwwlklem2  30032  clwwisshclwws  30047  erclwwlktr  30054  clwwlkel  30078  clwwlkext2edg  30088  erclwwlkntr  30103  clwlknf1oclwwlknlem2  30114  clwlknf1oclwwlknlem3  30115  clwlknf1oclwwlkn  30116  clwwlknonccat  30128  0wlkons1  30153  3wlkdlem6  30197  eupth2eucrct  30249  frgrwopreglem2  30345  2clwwlk2clwwlk  30382  wlkl0  30399  nvmul0or  30682  ipasslem5  30867  ipasslem11  30872  hvmul0or  31057  his6  31131  hhssnv  31296  ocsh  31315  ocin  31328  shsidmi  31416  chnlen0  31476  h1de2bi  31586  h1de2ctlem  31587  h1de2ci  31588  spansni  31589  3oalem1  31694  nmcexi  32058  atcveq0  32380  chcv1  32387  cdjreui  32464  cdj3lem2b  32469  xrge0tsmsd  33041  1fldgenq  33289  ccfldextdgrr  33682  ordtrest2NEWlem  33868  ordtrest2NEW  33869  xrge0iifcnv  33879  esumc  34015  esumpcvgval  34042  ballotlemfc0  34457  ballotlemfcc  34458  gblacfnacd  35075  subfacp1lem4  35151  subfacp1lem5  35152  erdszelem8  35166  sconnpi1  35207  cvmsss2  35242  cvmlift2lem12  35282  satfv0  35326  satfv0fun  35339  satf00  35342  sat1el2xp  35347  fmla0xp  35351  fmlasucdisj  35367  satffunlem1lem1  35370  satffunlem2lem1  35372  dmopab3rexdif  35373  msubco  35499  msubvrs  35528  ellcsrspsn  35609  sinccvglem  35640  untsucf  35672  nnuni  35689  dfrdg2  35759  colineardim1  36025  btwnconn1lem14  36064  segleantisym  36079  colinbtwnle  36082  outsidele  36096  lineunray  36111  linethru  36117  elicc3  36283  opnregcld  36296  cldregopn  36297  fnejoin2  36335  bj-isrvec  37260  dissneqlem  37306  icorempo  37317  relowlssretop  37329  relowlpssretop  37330  rdgssun  37344  finxpsuclem  37363  lindsenlbs  37575  ptrecube  37580  poimirlem6  37586  poimirlem7  37587  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  itg2addnclem3  37633  ftc1anclem6  37658  dvasin  37664  unirep  37674  sdclem2  37702  ssbnd  37748  prdsbnd  37753  cntotbnd  37756  heibor1lem  37769  rrnequiv  37795  ismndo2  37834  grpoeqdivid  37841  isdrngo3  37919  crngohomfo  37966  0idl  37985  1idl  37986  divrngidl  37988  smprngopr  38012  prnc  38027  ispridlc  38030  riotaclbgBAD  38910  lshpdisj  38943  lsateln0  38951  lsatcveq0  38988  opnlen0  39144  cmtbr4N  39211  cvrnbtwn2  39231  cvrnbtwn4  39235  atcvreq0  39270  cvlatexch1  39292  exatleN  39361  atlelt  39395  ps-2  39435  llnn0  39473  lplnn0N  39504  islpln2a  39505  lvoln0N  39548  islvol2aN  39549  4at  39570  dalemcea  39617  dalem3  39621  pmapglb2N  39728  pmapglb2xN  39729  cdlema1N  39748  cdlemb  39751  paddasslem17  39793  llnexchb2lem  39825  llnexchb2  39826  lhpat3  40003  ltrnid  40092  trlne  40142  cdlemc4  40151  cdleme11h  40223  cdlemednuN  40257  cdlemg1a  40527  tendoeq2  40731  tendoid0  40782  dva1dim  40942  dib1dim  41122  dihlatat  41294  dochkrshp4  41346  dochkr1  41435  lclkrlem2e  41468  lcfrlem16  41515  lcfrlem28  41527  mapd0  41622  hdmap14lem13  41837  fnsnbt  42225  eqresfnbd  42227  f1o2d2  42228  expeq1d  42311  expeqidd  42312  dvdsexpnn0  42321  reladdrsub  42361  sn-negex12  42392  sn-mullid  42411  sn-mul02  42416  nn0addcom  42426  nn0mulcom  42430  zmulcomlem  42431  mulgt0con1d  42434  mulgt0con2d  42435  sn-sup2  42447  frlmsnic  42495  evlselvlem  42541  prjspner1  42581  elrfi  42650  mrefg2  42663  eldiophb  42713  eldioph2b  42719  diophin  42728  diophun  42729  rexzrexnn0  42760  eldioph4b  42767  diophren  42769  rencldnfilem  42776  pellexlem6  42790  jm2.19  42950  rmydioph  42971  expdiophlem1  42978  expdioph  42980  lnr2i  43073  lpirlnr  43074  hbtlem2  43081  hbtlem4  43083  hbtlem6  43086  dgrsub2  43092  dgraa0p  43106  rngunsnply  43130  nlimsuc  43403  dfsucon  43485  radcnvrat  44283  pm14.24  44401  addrcom  44444  natlocalincr  46795  afveu  47068  dfafn5b  47076  rlimdmafv  47092  afv2eu  47153  rlimdmafv2  47173  el1fzopredsuc  47240  elsetpreimafvssdm  47260  imasetpreimafvbijlemfo  47279  sprvalpw  47354  prprvalpw  47389  reupr  47396  fmtnofac2lem  47442  proththdlem  47487  perfectALTVlem2  47596  perfectALTV  47597  gbowpos  47633  gbowgt5  47636  gboge9  47638  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  isuspgrim0  47756  isuspgrimlem  47758  clnbgrgrim  47786  grimedg  47787  grtrissvtx  47795  grlimgrtrilem2  47819  ringcinvALTV  48033  lincellss  48155  lindsrng01  48197  suppdm  48239  nnpw2pb  48321  0aryfvalel  48368  0aryfvalelfv  48369  itsclc0xyqsolr  48503