Theorem syl5ibrcom 250

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 249	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
4	3	com12 33	1 ⊢ (𝜑 → (𝜒 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimprcd  253  iftrueb  4502  elsn2g  4632  preq1b  4813  elpreqprb  4835  reusv3  5378  alxfr  5380  reuhypd  5392  axpr  5400  opth1  5459  euotd  5498  otiunsndisj  5505  tz7.2  5646  frsn  5751  dmopab2rex  5909  elsnxp  6296  reuop  6298  dfpo2  6301  ordtri1  6398  ordtri3  6401  fvmptdv2  7012  fveqressseq  7078  foco2  7108  fsn  7135  fnsnbg  7166  fnsnbOLD  7168  fmptsng  7170  fmptsnd  7171  fconst2g  7205  fnprb  7210  fntpb  7211  funfvima  7232  soisoi  7332  isores3  7339  eqfunresadj  7366  riotaeqimp  7399  eusvobj2  7408  ovmpodv2  7574  f1opw2  7671  sorpssun  7733  sorpssin  7734  oneqmin  7801  nlimsucg  7840  onzsl  7844  tfinds  7858  funcnvuni  7931  mptcnfimad  7985  opiota  8058  mposn  8100  mpof1o2d  8123  frpoins3xpg  8138  frpoins3xp3g  8139  poxp2  8141  xpord2pred  8143  sexp2  8144  poxp3  8148  xpord3pred  8150  sexp3  8151  xpord3inddlem  8152  suppssov1  8195  suppssov2  8196  suppssfv  8200  brtpos  8233  frrlem12  8296  frrlem13  8297  seqomlem1  8439  seqomlem2  8440  omordi  8553  omord  8555  omwordi  8558  oeeui  8590  nnmordi  8619  nnmord  8620  nnmwordi  8623  nnawordex  8625  nnaordex  8626  nneob  8644  omsmolem  8645  eldifsucnn  8652  qsss  8775  eroveu  8812  mapsncnv  8893  ralxpmap  8896  elixpsn  8937  ixpsnf1o  8938  boxcutc  8941  pw2f1olem  9072  2pwne  9124  mapxpen  9134  mapunen  9137  php  9194  onomeneq  9201  unxpdomlem2  9220  en1eqsnbi  9239  isfiniteg  9263  fofinf1o  9292  f1opwfi  9316  elfiun  9393  oieu  9504  brwdom2  9538  wdomtr  9540  ixpiunwdom  9555  en3lplem1  9584  suc11reg  9591  inf3lemd  9599  cantnfvalf  9637  cantnflt  9644  cantnfp1lem3  9652  cantnflem2  9662  ttrcltr  9688  rnttrcl  9694  ttrclselem1  9697  r1tr  9751  updjud  9932  dfac8alem  10025  wdomnumr  10060  isinfcard  10088  aceq3lem  10116  dfac5lem4  10122  dfac5  10124  dfac2b  10126  coftr  10268  fin23lem28  10335  fin23lem29  10336  fin1a2lem11  10405  fin1a2lem12  10406  fin1a2lem13  10407  hsmexlem9  10420  axdclem  10514  pwcfsdom  10579  gchdomtri  10625  fpwwe2  10639  gchpwdom  10666  gchhar  10675  addnidpi  10897  nqereu  10925  genpv  10995  genpdm  10998  distrlem5pr  11023  mulrid  11217  ltne  11318  mul02  11399  cnegex  11402  mul0or  11865  negfi  12175  sup2  12182  supaddc  12193  supadd  12194  supmul1  12195  supmul  12198  creur  12223  creui  12224  cju  12225  nnsub  12291  un0addcl  12548  un0mulcl  12549  nn0sub  12565  elz2  12620  zaddcl  12645  suprzcl2  12974  qmulz  12987  qre  12989  qnegcl  13002  elpqb  13012  xrmax1  13213  xrmin2  13216  max1ALT  13224  xlesubadd  13301  xmulass  13325  xlemul1a  13326  xrsupexmnf  13343  xrinfmexpnf  13344  xrub  13350  iccid  13429  fzsn  13607  fzsuc2  13623  fz1sbc  13641  elfzp12  13644  modmuladd  13963  seqid3  14096  bcval5  14368  bcpasc  14371  hashbnd  14386  hashnnn0genn0  14393  hashprg  14445  hashfzo  14480  tpfo  14551  wrdl1s1  14668  ccats1alpha  14673  cats1un  14776  s7f1o  15023  shftlem  15125  replim  15187  absmod0  15374  absz  15382  rlimdm  15622  summolem2  15786  summo  15787  zsum  15788  fsum  15790  fsummulc2  15854  fsumconst  15860  fsum00  15869  incexclem  15909  isumsplit  15913  infcvgaux1i  15930  prodmolem2  16008  prodmo  16009  zprod  16010  fprod  16014  prodsn  16035  prodsnf  16037  fprodconst  16051  ruclem2  16306  fzo0dvdseq  16399  bitsf1ocnv  16520  sadcaddlem  16533  smueqlem  16566  gcdabs1  16605  bezoutlem1  16615  bezoutlem3  16617  bezoutlem4  16618  dvdsgcd  16620  dvdsmulgcd  16632  lcmgcdeq  16688  lcmf  16709  lcmfunsnlem1  16713  lcmfunsnlem2lem2  16715  isprm2lem  16757  dvdsprime  16763  isprm5  16784  coprm  16788  prmdvdsexpr  16794  rpexp  16799  phibndlem  16847  dfphi2  16851  hashgcdlem  16865  odzdvds  16873  nnoddn2prm  16889  pythagtriplem1  16894  iserodd  16913  pceulem  16923  pcqmul  16931  pcqcl  16934  pcxnn0cl  16938  pcxcl  16939  pcneg  16952  pcabs  16953  pcgcd1  16955  pcz  16959  pcprmpw2  16960  pcprmpw  16961  dvdsprmpweqle  16964  difsqpwdvds  16965  pcaddlem  16966  pcadd  16967  pcmpt  16970  pockthg  16984  prmreclem5  16998  4sqlem4  17030  mul4sq  17032  vdwapun  17052  vdwlem2  17060  vdwlem6  17064  vdwlem8  17066  vdwlem13  17071  0ram  17098  ram0  17100  ramcl  17107  cshwsiun  17177  wunress  17327  firest  17503  isssc  17895  pospo  18417  latnlej  18530  gsumval2a  18765  xpsmnd0  18860  mnd1id  18862  0subm  18900  mulgnn0p1  19175  mulgnn0ass  19200  cyccom  19298  gicsubgen  19373  symg1bas  19485  snsymgefmndeq  19489  psgnunilem1  19587  psgnunilem2  19589  mndodcongi  19637  oddvdsnn0  19638  odnncl  19639  oddvds  19641  odeq  19644  odeq1  19654  pgpfi2  19700  sylow2a  19713  sylow2blem3  19716  sylow3lem6  19726  lsmelvalm  19745  lsmsubm  19747  lsmsubg  19748  lsmmod  19769  lsmdisj2  19776  efgmnvl  19808  efgtlen  19820  efgs1b  19830  efgrelexlemb  19844  efgredeu  19846  efgcpbllemb  19849  frgpuptinv  19865  frgpup3lem  19871  qusabl  19959  frgpnabllem1  19967  cyggeninv  19977  cyggenod  19978  gsumval3eu  19998  dprdssv  20112  dprdfeq0  20118  dprdsubg  20120  dprddisj2  20135  ablfacrp  20162  pgpfac1lem3  20173  pgpfaclem2  20178  xpsring1d  20441  dvreq1  20519  irredn1  20534  crngrhmfo  20604  nzrunit  20652  ringcinv  20800  rrgeq0  20829  domneq0  20837  isdrng5  20884  isabvd  20945  abvdom  20963  issrngd  20988  lmodfopnelem2  21050  lss1d  21114  lspsneq0  21163  lbspss  21233  lsmcl  21234  lvecvs0or  21262  lspindpi  21286  lidl1el  21381  rspsn0  21402  lpiss  21527  lidldvgen  21532  qsssubdrg  21606  zringlpirlem1  21642  pzriprnglem6  21666  pzriprnglem12  21672  znfld  21740  znunit  21743  znrrg  21745  cygznlem3  21749  frgpcyg  21753  psgnghm  21760  ipeq0  21818  cssincl  21868  lsmcss  21872  obselocv  21908  dsmmacl  21921  dsmmlss  21924  mplsubrglem  22183  mplmonmul  22217  mplcoe5lem  22220  mhpsclcl  22340  mhpvarcl  22341  psdmul  22359  coe1tmmul2  22467  coe1tmmul  22468  pf1ind  22545  mat1dimelbas  22658  mdetralt  22795  mdetunilem2  22800  mdetunilem7  22805  mdetunilem9  22807  maducoeval2  22827  chpscmat  23029  chfacfscmulgsum  23047  chfacfpmmulgsum  23051  istopon  23099  eltg3  23149  tgidm  23167  clsval2  23237  opncldf1  23271  restbas  23345  tgrest  23346  restcld  23359  restcldr  23361  restcls  23368  restntr  23369  ordtbas2  23378  ordtbas  23379  ordtrest2lem  23390  ordtrest2  23391  pnfnei  23407  mnfnei  23408  tgcn  23439  cnconst  23471  cnindis  23479  lmss  23485  ordtt1  23566  discmp  23585  1stcrest  23640  2ndcdisj  23644  cldllycmp  23683  txbas  23755  ptpjpre1  23759  ptuni2  23764  ptbasin  23765  ptbasfi  23769  ptopn2  23772  txbasval  23794  ptpjopn  23800  ptclsg  23803  dfac14lem  23805  xkoccn  23807  ptcnp  23810  upxp  23811  ptrescn  23827  txkgen  23840  xkoptsub  23842  xkopt  23843  xkoco1cn  23845  xkoco2cn  23846  xkococn  23848  xkoinjcn  23875  ordthmeolem  23989  ptuncnv  23995  nrmhaus  24014  fbssint  24026  fbfinnfr  24029  fbasrn  24072  isufil2  24096  filufint  24108  rnelfm  24141  fmfnfmlem2  24143  fmfnfmlem3  24144  fmfnfmlem4  24145  fmfnfm  24146  flimtopon  24158  flimclslem  24172  fclstopon  24200  fclscf  24213  flimfnfcls  24216  alexsublem  24232  alexsubALTlem3  24237  alexsubALTlem4  24238  ptcmplem2  24241  tmdgsum2  24284  symgtgp  24294  cldsubg  24299  qustgplem  24309  tgptsmscld  24339  tsmsxplem1  24341  imasdsf1olem  24561  blssps  24612  blss  24613  stdbdxmet  24703  methaus  24708  metrest  24712  nrginvrcn  24880  nmoeq0  24924  blssioo  24983  xrtgioo  24995  xrsxmet  24998  reconnlem1  25015  reconnlem2  25016  xrge0tsms  25023  elcncf1di  25085  iccpnfcnv  25134  evth  25149  lebnumlem1  25151  lebnumlem2  25152  lebnumlem3  25153  nmoleub3  25309  minveclem3b  25618  ivthlem2  25642  ivthlem3  25643  elovolm  25665  ovolmge0  25667  ovoliun  25695  ovolicc2lem3  25709  ovolicc2  25712  voliunlem3  25742  dyaddisj  25786  dyadmax  25788  opnmblALT  25793  ismbfd  25829  ismbf2d  25830  mbfimaopnlem  25845  mbfimaopn2  25847  i1fmullem  25884  i1fres  25895  itg1climres  25904  mbfi1fseqlem4  25908  itg2lcl  25917  itgsplitioo  26028  ellimc2  26067  rolle  26180  dvlip  26183  dvge0  26196  dvne0  26201  lhop1lem  26203  tdeglem4  26248  degltlem1  26260  deg1nn0clb  26278  deg1lt0  26279  dvdsq1p  26351  ply1rem  26354  fta1g  26358  elply2  26384  plyf  26386  ne0p  26395  plyeq0lem  26398  plypf1  26400  0dgrb  26434  coe1termlem  26446  dgrcolem2  26462  plymul0or  26470  plyrem  26497  fta1  26500  quotcan  26501  aalioulem3  26528  eff1olem  26744  lognegb  26786  eflogeq  26798  argregt0  26806  argrege0  26807  tanarg  26815  cxpexp  26864  cxpeq0  26874  mulcxp  26881  cxpeq  26953  atans2  27127  scvxcvx  27181  dmgmaddn0  27218  isppw2  27310  vmappw  27311  vmacl  27313  efvmacl  27315  isnsqf  27330  mumullem2  27375  sqff1o  27377  dvdsppwf1o  27381  ppiublem1  27397  vmalelog  27400  chtublem  27406  fsumvma  27408  perfectlem2  27425  perfect  27426  bposlem1  27479  lgsmod  27518  lgsne0  27530  lgsdirnn0  27539  lgsqr  27546  lgsdchr  27550  gausslemma2dlem1a  27560  gausslemma2dlem6  27567  lgseisenlem2  27571  lgsquadlem1  27575  lgsquadlem2  27576  2lgslem1b  27587  2sqlem2  27613  mul2sq  27614  2sqlem7  27619  dchrisum0fno1  27706  pntrsumbnd2  27762  ostthlem1  27822  ostth2lem2  27829  ostth3  27833  ostth  27834  nolesgn2ores  27867  nogesgn1ores  27869  nolt02o  27890  nogt01o  27891  nosupbnd2  27911  noinfbnd2lem1  27925  noetasuplem4  27931  noetainflem4  27935  maxs1  27964  mins2  27967  ltsne  27969  eqcuts3  28028  cuteq1  28041  madef  28060  ltslpss  28132  lrrecfr  28167  addsval  28186  addsproplem2  28194  addsuniflem  28225  addbdaylem  28241  negsid  28265  negsunif  28279  mulsproplem5  28344  mulsproplem6  28345  mulsproplem7  28346  mulsproplem8  28347  mulsproplem9  28348  lemulsd  28362  sltmuls1  28371  sltmuls2  28372  ltmuls2  28395  muls0ord  28409  precsexlem8  28438  precsexlem9  28439  precsexlem11  28441  elons2  28482  oncutlt  28488  bdayons  28500  onaddscl  28501  onmulscl  28502  nnsge1  28567  n0fincut  28579  n0subs  28587  dfnns2  28596  eucliddivs  28600  znegscl  28616  zaddscl  28618  zmulscld  28621  elzn0s  28622  eln0zs  28624  n0seo  28645  zseo  28646  bdaypw2n0bndlem  28687  bdaypw2n0bnd  28688  z12no  28700  z12addscl  28701  z12negscl  28702  z12shalf  28704  z12zsodd  28706  z12sge0  28707  z12bdaylem  28708  bdayfinlem  28710  recut  28718  elreno2  28719  remulscllem1  28724  colinearalg  29291  axpasch  29322  axlowdimlem16  29338  axlowdimlem17  29339  axlowdim  29342  axcontlem2  29346  axcontlem4  29348  axcontlem7  29351  lpvtx  29449  edglnl  29524  numedglnl  29525  usgredgop  29554  usgrexmplef  29643  uhgrspansubgrlem  29674  uhgrspan1  29687  nbusgredgeu0  29752  nb3grprlem2  29765  cusgrsize2inds  29837  vtxd0nedgb  29872  rusgrpropnb  29967  upgrwlkvtxedg  30028  wlkp1lem1  30055  wlkp1lem6  30060  wlkp1lem8  30062  usgr2wlkneq  30145  crctcshwlk  30214  crctcsh  30216  iswwlksnon  30245  wlkiswwlks1  30259  wwlksnextbi  30286  wwlksnextproplem2  30302  wspthsnonn0vne  30309  clwlkclwwlklem2  30394  clwwisshclwws  30409  erclwwlktr  30416  clwwlkel  30440  clwwlkext2edg  30450  erclwwlkntr  30465  clwlknf1oclwwlknlem2  30476  clwlknf1oclwwlknlem3  30477  clwlknf1oclwwlkn  30478  clwwlknonccat  30490  0wlkons1  30515  3wlkdlem6  30563  eupth2eucrct  30615  frgrwopreglem2  30711  2clwwlk2clwwlk  30748  wlkl0  30765  nvmul0or  31049  ipasslem5  31234  ipasslem11  31239  hvmul0or  31424  his6  31498  hhssnv  31663  ocsh  31682  ocin  31695  shsidmi  31783  chnlen0  31843  h1de2bi  31953  h1de2ctlem  31954  h1de2ci  31955  spansni  31956  3oalem1  32061  nmcexi  32425  atcveq0  32747  chcv1  32754  cdjreui  32831  cdj3lem2b  32836  xrge0tsmsd  33433  1fldgenq  33683  psrmonmul  33980  ccfldextdgrr  34102  ordtrest2NEWlem  34352  ordtrest2NEW  34353  xrge0iifcnv  34363  esumc  34481  esumpcvgval  34508  ballotlemfc0  34924  ballotlemfcc  34925  fissorduni  35514  axprALT2  35537  fineqvnttrclse  35570  gblacfnacd  35619  vonf1oonfo  35632  onvfowev  35633  subfacp1lem4  35688  subfacp1lem5  35689  erdszelem8  35703  sconnpi1  35744  cvmsss2  35779  cvmlift2lem12  35819  satfv0  35863  satfv0fun  35876  satf00  35879  sat1el2xp  35884  fmla0xp  35888  fmlasucdisj  35904  satffunlem1lem1  35907  satffunlem2lem1  35909  dmopab3rexdif  35910  msubco  36036  msubvrs  36065  ellcsrspsn  36146  sinccvglem  36177  untsucf  36215  nnuni  36232  dfrdg2  36298  colineardim1  36566  btwnconn1lem14  36605  segleantisym  36620  colinbtwnle  36623  outsidele  36637  lineunray  36652  linethru  36658  nmulprop  36695  nmuladdss  36718  elicc3  36861  opnregcld  36874  cldregopn  36875  fnejoin2  36913  bj-isrvec  37971  dissneqlem  38019  icorempo  38030  relowlssretop  38042  relowlpssretop  38043  rdgssun  38057  finxpsuclem  38076  lindsenlbs  38299  ptrecube  38304  poimirlem6  38310  poimirlem7  38311  poimirlem16  38320  poimirlem17  38321  poimirlem19  38323  poimirlem20  38324  poimirlem21  38325  poimirlem22  38326  poimirlem23  38327  poimirlem24  38328  poimirlem25  38329  poimirlem26  38330  poimirlem27  38331  poimirlem29  38333  poimirlem30  38334  poimirlem31  38335  poimirlem32  38336  itg2addnclem3  38357  ftc1anclem6  38382  dvasin  38388  unirep  38398  sdclem2  38426  ssbnd  38472  prdsbnd  38477  cntotbnd  38480  heibor1lem  38493  rrnequiv  38519  ismndo2  38558  grpoeqdivid  38565  isdrngo3  38643  crngohomfo  38690  0idl  38709  1idl  38710  divrngidl  38712  smprngopr  38736  prnc  38751  ispridlc  38754  disjimeceqim  39486  riotaclbgBAD  39761  lshpdisj  39794  lsateln0  39802  lsatcveq0  39839  opnlen0  39995  cmtbr4N  40062  cvrnbtwn2  40082  cvrnbtwn4  40086  atcvreq0  40121  cvlatexch1  40143  exatleN  40211  atlelt  40245  ps-2  40285  llnn0  40323  lplnn0N  40354  islpln2a  40355  lvoln0N  40398  islvol2aN  40399  4at  40420  dalemcea  40467  dalem3  40471  pmapglb2N  40578  pmapglb2xN  40579  cdlema1N  40598  cdlemb  40601  paddasslem17  40643  llnexchb2lem  40675  llnexchb2  40676  lhpat3  40853  ltrnid  40942  trlne  40992  cdlemc4  41001  cdleme11h  41073  cdlemednuN  41107  cdlemg1a  41377  tendoeq2  41581  tendoid0  41632  dva1dim  41792  dib1dim  41972  dihlatat  42144  dochkrshp4  42196  dochkr1  42285  lclkrlem2e  42318  lcfrlem16  42365  lcfrlem28  42377  mapd0  42472  hdmap14lem13  42687  eqresfnbd  43036  expeq1d  43118  expeqidd  43119  dvdsexpnn0  43128  reladdrsub  43179  sn-remul0ord  43202  sn-negex12  43211  sn-mullid  43230  sn-mul02  43259  nn0addcom  43269  nn0mulcom  43273  zmulcomlem  43274  mulgt0con1d  43277  mulgt0con2d  43278  sn-sup2  43298  frlmsnic  43341  evlselvlem  43353  prjspner1  43391  elrfi  43458  mrefg2  43471  eldiophb  43521  eldioph2b  43527  diophin  43536  diophun  43537  rexzrexnn0  43564  eldioph4b  43571  diophren  43573  rencldnfilem  43580  pellexlem6  43594  jm2.19  43753  rmydioph  43774  expdiophlem1  43781  expdioph  43783  lnr2i  43876  lpirlnr  43877  hbtlem2  43884  hbtlem4  43886  hbtlem6  43889  dgrsub2  43895  dgraa0p  43909  rngunsnply  43929  nlimsuc  44200  dfsucon  44282  radcnvrat  45057  pm14.24  45175  addrcom  45216  modelaxreplem1  45720  ormklocald  47623  natlocalincr  47625  afveu  47923  dfafn5b  47931  rlimdmafv  47947  afv2eu  48008  rlimdmafv2  48028  el1fzopredsuc  48096  minusmod5ne  48125  modmknepk  48138  elsetpreimafvssdm  48168  imasetpreimafvbijlemfo  48187  sprvalpw  48262  prprvalpw  48297  reupr  48304  fmtnofac2lem  48353  proththdlem  48398  perfectALTVlem2  48520  perfectALTV  48521  gbowpos  48557  gbowgt5  48560  gboge9  48562  nnsum4primesodd  48594  nnsum4primesoddALTV  48595  uhgrimedgi  48688  isuspgrim0  48692  isuspgrimlem  48693  upgrimpths  48707  clnbgrgrim  48732  grimedg  48733  grtrissvtx  48742  stgredgiun  48756  stgrvtx0  48760  isubgr3stgrlem7  48770  grlimgrtrilem2  48800  gpgiedgdmellem  48844  gpgvtxel2  48846  gpgvtx0  48851  gpgvtx1  48852  gpgusgralem  48854  gpgedgvtx0  48859  gpgedgvtx1  48860  gpgedg2ov  48864  gpgedg2iv  48865  gpgnbgrvtx0  48872  gpgnbgrvtx1  48873  pgnbgreunbgr  48923  ringcinvALTV  49108  smprngprmrng  49137  lincellss  49239  lindsrng01  49281  suppdm  49323  nnpw2pb  49400  0aryfvalel  49447  0aryfvalelfv  49448  itsclc0xyqsolr  49582  infsubc  49871  infsubc2  49872