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  4494  elsn2g  4621  preq1b  4800  elpreqprb  4822  reusv3  5367  alxfr  5369  reuhypd  5381  axpr  5389  opth1  5444  euotd  5486  otiunsndisj  5493  tz7.2  5634  frsn  5740  dmopab2rex  5900  elsnxp  6297  reuop  6299  dfpo2  6302  ordtri1  6399  ordtri3  6402  fvmptdv2  7017  fveqressseq  7084  foco2  7114  fsn  7141  fnsnbg  7174  fmptsng  7177  fmptsnd  7178  fconst2g  7213  fnprb  7218  fntpb  7219  funfvima  7240  soisoi  7340  isores3  7347  eqfunresadj  7374  riotaeqimp  7407  eusvobj2  7416  ovmpodv2  7582  f1opw2  7680  sorpssun  7750  sorpssin  7751  oneqmin  7818  nlimsucg  7857  onzsl  7861  tfinds  7875  funcnvuni  7948  mptcnfimad  8002  opiota  8074  mposn  8120  mpof1o2d  8143  frpoins3xpg  8163  frpoins3xp3g  8164  poxp2  8166  xpord2pred  8168  sexp2  8169  poxp3  8173  xpord3pred  8175  sexp3  8176  xpord3inddlem  8177  suppssov1  8221  suppssov2  8222  suppssfv  8226  brtpos  8259  frrlem12  8322  frrlem13  8323  seqomlem1  8467  seqomlem2  8468  omordi  8581  omord  8583  omwordi  8586  oeeui  8618  nnmordi  8647  nnmord  8648  nnmwordi  8651  nnawordex  8653  nnaordex  8654  nneob  8672  omsmolem  8673  eldifsucnn  8680  qsss  8803  eroveu  8840  mapsncnv  8928  ralxpmap  8931  elixpsn  8972  ixpsnf1o  8973  boxcutc  8976  pw2f1olem  9107  2pwne  9159  mapxpen  9169  mapunen  9172  php  9229  onomeneq  9236  unxpdomlem2  9255  en1eqsnbi  9274  fissorduni  9289  isfiniteg  9299  fofinf1o  9328  f1opwfi  9352  elfiun  9429  oieu  9540  brwdom2  9574  wdomtr  9576  ixpiunwdom  9591  en3lplem1  9620  suc11reg  9627  inf3lemd  9635  cantnfvalf  9673  cantnflt  9680  cantnfp1lem3  9688  cantnflem2  9698  ttrcltr  9724  rnttrcl  9730  ttrclselem1  9733  r1tr  9790  updjud  10022  dfac8alem  10115  wdomnumr  10150  isinfcard  10178  aceq3lem  10206  dfac5lem4  10212  dfac5  10214  dfac2b  10216  coftr  10358  fin23lem28  10425  fin23lem29  10426  fin1a2lem11  10495  fin1a2lem12  10496  fin1a2lem13  10497  hsmexlem9  10510  axdclem  10604  pwcfsdom  10675  gchdomtri  10721  fpwwe2  10735  gchpwdom  10762  gchhar  10771  addnidpi  10993  nqereu  11021  genpv  11091  genpdm  11094  distrlem5pr  11119  mulrid  11313  ltne  11414  mul02  11495  cnegex  11498  mul0or  11963  negfi  12273  sup2  12280  supaddc  12291  supadd  12292  supmul1  12293  supmul  12296  creur  12321  creui  12322  cju  12323  nnsub  12389  un0addcl  12646  un0mulcl  12647  nn0sub  12663  elz2  12718  zaddcl  12743  suprzcl2  13072  qmulz  13085  qre  13087  qnegcl  13101  elpqb  13111  xrmax1  13312  xrmin2  13315  max1ALT  13323  xlesubadd  13400  xmulass  13424  xlemul1a  13425  xrsupexmnf  13442  xrinfmexpnf  13443  xrub  13449  iccid  13528  fzsn  13707  fzsuc2  13723  fz1sbc  13741  elfzp12  13744  modmuladd  14063  seqid3  14196  bcval5  14469  bcpasc  14472  hashbnd  14487  hashnnn0genn0  14494  hashprg  14546  hashfzo  14581  tpfo  14652  wrdl1s1  14770  ccats1alpha  14775  cats1un  14878  s7f1o  15128  shftlem  15230  replim  15292  absmod0  15479  absz  15487  rlimdm  15727  summolem2  15891  summo  15892  zsum  15893  fsum  15895  fsummulc2  15959  fsumconst  15965  fsum00  15974  incexclem  16014  isumsplit  16018  infcvgaux1i  16035  prodmolem2  16111  prodmo  16112  zprod  16113  fprod  16117  prodsn  16138  prodsnf  16140  fprodconst  16154  ruclem2  16409  fzo0dvdseq  16502  bitsf1ocnv  16623  sadcaddlem  16636  smueqlem  16669  gcdabs1  16711  bezoutlem1  16721  bezoutlem3  16723  bezoutlem4  16724  dvdsgcd  16726  dvdsmulgcd  16739  lcmgcdeq  16796  lcmf  16817  lcmfunsnlem1  16821  lcmfunsnlem2lem2  16823  isprm2lem  16865  dvdsprime  16871  isprm5  16892  coprm  16896  prmdvdsexpr  16902  rpexp  16907  phibndlem  16956  dfphi2  16960  hashgcdlem  16974  odzdvds  16982  nnoddn2prm  16998  pythagtriplem1  17003  iserodd  17022  pceulem  17032  pcqmul  17040  pcqcl  17043  pcxnn0cl  17047  pcxcl  17048  pcneg  17061  pcabs  17062  pcgcd1  17064  pcz  17068  pcprmpw2  17069  pcprmpw  17070  dvdsprmpweqle  17073  difsqpwdvds  17074  pcaddlem  17075  pcadd  17076  pcmpt  17079  pockthg  17093  prmreclem5  17107  4sqlem4  17139  mul4sq  17141  vdwapun  17161  vdwlem2  17169  vdwlem6  17173  vdwlem8  17175  vdwlem13  17180  0ram  17207  ram0  17209  ramcl  17216  cshwsiun  17286  wunress  17436  firest  17612  isssc  18004  pospo  18526  latnlej  18639  gsumval2a  18883  xpsmnd0  18981  mnd1id  18983  0subm  19022  mulgnn0p1  19304  mulgnn0ass  19329  cyccom  19427  gicsubgen  19502  symg1bas  19614  snsymgefmndeq  19618  psgnunilem1  19716  psgnunilem2  19718  mndodcongi  19766  oddvdsnn0  19767  odnncl  19768  oddvds  19770  odeq  19773  odeq1  19783  pgpfi2  19829  sylow2a  19842  sylow2blem3  19845  sylow3lem6  19855  lsmelvalm  19874  lsmsubm  19876  lsmsubg  19877  lsmmod  19898  lsmdisj2  19905  efgmnvl  19937  efgtlen  19949  efgs1b  19959  efgrelexlemb  19973  efgredeu  19975  efgcpbllemb  19978  frgpuptinv  19994  frgpup3lem  20000  qusabl  20088  frgpnabllem1  20096  cyggeninv  20106  cyggenod  20107  gsumval3eu  20127  dprdssv  20241  dprdfeq0  20247  dprdsubg  20249  dprddisj2  20264  ablfacrp  20291  pgpfac1lem3  20302  pgpfaclem2  20307  xpsring1d  20572  dvreq1  20650  irredn1  20665  crngrhmfo  20735  nzrunit  20784  ringcinv  20932  rrgeq0  20961  domneq0  20969  isdrng5  21017  isabvd  21078  abvdom  21096  issrngd  21121  lmodfopnelem2  21183  lss1d  21247  lspsneq0  21296  lbspss  21366  lsmcl  21367  lvecvs0or  21395  lspindpi  21419  lidl1el  21514  rspsn0  21535  lpiss  21662  lidldvgen  21667  qsssubdrg  21741  zringlpirlem1  21777  pzriprnglem6  21801  pzriprnglem12  21807  znfld  21875  znunit  21878  znrrg  21880  cygznlem3  21884  frgpcyg  21888  psgnghm  21895  ipeq0  21953  cssincl  22003  lsmcss  22007  obselocv  22043  dsmmacl  22056  dsmmlss  22059  lindsenlbs  22166  mplsubrglem  22320  mplmonmul  22354  mplcoe5lem  22357  mhpsclcl  22477  mhpvarcl  22478  psdmul  22496  coe1tmmul2  22604  coe1tmmul  22605  pf1ind  22682  mat1dimelbas  22795  mdetralt  22932  mdetunilem2  22937  mdetunilem7  22942  mdetunilem9  22944  maducoeval2  22964  chpscmat  23169  chfacfscmulgsum  23187  chfacfpmmulgsum  23191  istopon  23239  eltg3  23289  tgidm  23307  clsval2  23377  opncldf1  23411  restbas  23485  tgrest  23486  restcld  23499  restcldr  23501  restcls  23508  restntr  23509  ordtbas2  23518  ordtbas  23519  ordtrest2lem  23530  ordtrest2  23531  pnfnei  23547  mnfnei  23548  tgcn  23579  cnconst  23611  cnindis  23619  lmss  23625  ordtt1  23706  discmp  23725  1stcrest  23780  2ndcdisj  23784  cldllycmp  23823  txbas  23895  ptpjpre1  23899  ptuni2  23904  ptbasin  23905  ptbasfi  23909  ptopn2  23912  txbasval  23934  ptpjopn  23940  ptclsg  23943  dfac14lem  23945  xkoccn  23947  ptcnp  23950  upxp  23951  ptrescn  23967  txkgen  23980  xkoptsub  23982  xkopt  23983  xkoco1cn  23985  xkoco2cn  23986  xkococn  23988  xkoinjcn  24015  ordthmeolem  24129  ptuncnv  24135  nrmhaus  24154  fbssint  24166  fbfinnfr  24169  fbasrn  24212  isufil2  24236  filufint  24248  rnelfm  24281  fmfnfmlem2  24283  fmfnfmlem3  24284  fmfnfmlem4  24285  fmfnfm  24286  flimtopon  24298  flimclslem  24312  fclstopon  24340  fclscf  24353  flimfnfcls  24356  alexsublem  24372  alexsubALTlem3  24377  alexsubALTlem4  24378  ptcmplem2  24381  tmdgsum2  24424  symgtgp  24434  cldsubg  24439  qustgplem  24449  tgptsmscld  24479  tsmsxplem1  24481  imasdsf1olem  24701  blssps  24752  blss  24753  stdbdxmet  24843  methaus  24848  metrest  24852  nrginvrcn  25020  nmoeq0  25064  blssioo  25123  xrtgioo  25135  xrsxmet  25138  reconnlem1  25155  reconnlem2  25156  xrge0tsms  25163  elcncf1di  25225  iccpnfcnv  25274  evth  25289  lebnumlem1  25291  lebnumlem2  25292  lebnumlem3  25293  nmoleub3  25449  minveclem3b  25758  ivthlem2  25782  ivthlem3  25783  elovolm  25805  ovolmge0  25807  ovoliun  25835  ovolicc2lem3  25849  ovolicc2  25852  voliunlem3  25882  dyaddisj  25926  dyadmax  25928  opnmblALT  25933  ismbfd  25969  ismbf2d  25970  mbfimaopnlem  25985  mbfimaopn2  25987  i1fmullem  26024  i1fres  26035  itg1climres  26044  mbfi1fseqlem4  26048  itg2lcl  26057  itgsplitioo  26167  ellimc2  26206  rolle  26319  dvlip  26322  dvge0  26335  dvne0  26340  lhop1lem  26342  tdeglem4  26387  degltlem1  26399  deg1nn0clb  26417  deg1lt0  26418  dvdsq1p  26490  ply1rem  26493  fta1g  26497  elply2  26523  plyf  26525  ne0p  26534  plyeq0lem  26538  plypf1  26540  0dgrb  26574  coe1termlem  26586  dgrcolem2  26602  plymul0or  26608  plyrem  26635  fta1  26638  rnplynfin  26639  quotcan  26641  aalioulem3  26670  eff1olem  26885  lognegb  26927  eflogeq  26939  argregt0  26947  argrege0  26948  tanarg  26956  cxpexp  27005  cxpeq0  27015  mulcxp  27022  cxpeq  27094  atans2  27268  scvxcvx  27322  dmgmaddn0  27359  isppw2  27451  vmappw  27452  vmacl  27454  efvmacl  27456  isnsqf  27471  mumullem2  27516  sqff1o  27518  dvdsppwf1o  27522  ppiublem1  27538  vmalelog  27541  chtublem  27547  fsumvma  27549  perfectlem2  27566  perfect  27567  bposlem1  27620  lgsmod  27659  lgsne0  27671  lgsdirnn0  27680  lgsqr  27687  lgsdchr  27691  gausslemma2dlem1a  27701  gausslemma2dlem6  27708  lgseisenlem2  27712  lgsquadlem1  27716  lgsquadlem2  27717  2lgslem1b  27728  2sqlem2  27754  mul2sq  27755  2sqlem7  27760  dchrisum0fno1  27847  pntrsumbnd2  27903  ostthlem1  27963  ostth2lem2  27970  ostth3  27974  ostth  27975  nolesgn2ores  28038  nogesgn1ores  28040  nolt02o  28061  nogt01o  28062  nosupbnd2  28082  noinfbnd2lem1  28096  noetasuplem4  28102  noetainflem4  28106  maxs1  28135  mins2  28138  ltsne  28140  eqcuts3  28199  cuteq1  28212  madef  28231  ltslpss  28303  lrrecfr  28338  addsval  28357  addsproplem2  28365  addsuniflem  28396  addbdaylem  28412  negsid  28436  negsunif  28450  mulsproplem5  28515  mulsproplem6  28516  mulsproplem7  28517  mulsproplem8  28518  mulsproplem9  28519  lemulsd  28533  sltmuls1  28542  sltmuls2  28543  ltmuls2  28566  muls0ord  28580  precsexlem8  28609  precsexlem9  28610  precsexlem11  28612  elons2  28653  oncutlt  28659  bdayons  28671  onaddscl  28672  onmulscl  28673  nnsge1  28738  n0fincut  28750  n0subs  28758  dfnns2  28767  eucliddivs  28771  znegscl  28787  zaddscl  28789  zmulscld  28792  elzn0s  28793  eln0zs  28795  n0seo  28816  zseo  28817  bdaypw2n0bndlem  28858  bdaypw2n0bnd  28859  z12no  28871  z12addscl  28872  z12negscl  28873  z12shalf  28875  z12zsodd  28877  z12sge0  28878  z12bdaylem  28879  bdayfinlem  28881  recut  28889  elreno2  28890  remulscllem1  28895  colinearalg  29497  axpasch  29528  axlowdimlem16  29544  axlowdimlem17  29545  axlowdim  29548  axcontlem2  29552  axcontlem4  29554  axcontlem7  29557  lpvtx  29655  edglnl  29730  numedglnl  29731  usgredgop  29760  usgrexmplef  29849  uhgrspansubgrlem  29880  uhgrspan1  29893  nbusgredgeu0  29958  nb3grprlem2  29971  cusgrsize2inds  30043  vtxd0nedgb  30078  rusgrpropnb  30173  upgrwlkvtxedg  30234  wlkp1lem1  30261  wlkp1lem6  30266  wlkp1lem8  30268  usgr2wlkneq  30351  crctcshwlk  30420  crctcsh  30422  iswwlksnon  30451  wlkiswwlks1  30465  wwlksnextbi  30492  wwlksnextproplem2  30508  wspthsnonn0vne  30515  clwlkclwwlklem2  30600  clwwisshclwws  30615  erclwwlktr  30622  clwwlkel  30646  clwwlkext2edg  30656  erclwwlkntr  30671  clwlknf1oclwwlknlem2  30682  clwlknf1oclwwlknlem3  30683  clwlknf1oclwwlkn  30684  clwwlknonccat  30696  0wlkons1  30721  3wlkdlem6  30775  eupth2eucrct  30827  frgrwopreglem2  30923  2clwwlk2clwwlk  30960  wlkl0  30977  nvmul0or  31261  ipasslem5  31446  ipasslem11  31451  hvmul0or  31636  his6  31710  hhssnv  31875  ocsh  31894  ocin  31907  shsidmi  31995  chnlen0  32055  h1de2bi  32165  h1de2ctlem  32166  h1de2ci  32167  spansni  32168  3oalem1  32273  nmcexi  32637  atcveq0  32959  chcv1  32966  cdjreui  33043  cdj3lem2b  33048  xrge0tsmsd  33684  1fldgenq  33934  psrmonmul  34232  ccfldextdgrr  34354  ordtrest2NEWlem  34604  ordtrest2NEW  34605  xrge0iifcnv  34615  esumc  34733  esumpcvgval  34760  ballotlemfc0  35175  ballotlemfcc  35176  axprALT2  35790  fineqvnttrclse  35852  gblacfnacd  35952  vonf1oonfo  35972  onvfowev  35973  subfacp1lem4  36038  subfacp1lem5  36039  erdszelem8  36053  sconnpi1  36094  cvmsss2  36129  cvmlift2lem12  36169  satfv0  36213  satfv0fun  36226  satf00  36229  sat1el2xp  36234  fmla0xp  36238  fmlasucdisj  36254  satffunlem1lem1  36257  satffunlem2lem1  36259  dmopab3rexdif  36260  msubco  36386  msubvrs  36415  ellcsrspsn  36496  sinccvglem  36527  mirimanoffr  36550  untsucf  36571  nnuni  36588  dfrdg2  36653  colineardim1  36922  btwnconn1lem14  36961  segleantisym  36976  colinbtwnle  36979  outsidele  36993  lineunray  37008  linethru  37014  nmulprop  37035  nmuladdss  37058  elicc3  37201  opnregcld  37214  cldregopn  37215  fnejoin2  37253  bj-isrvec  38324  dissneqlem  38372  icorempo  38383  relowlssretop  38395  relowlpssretop  38396  rdgssun  38410  finxpsuclem  38429  ptrecube  38647  poimirlem6  38653  poimirlem7  38654  poimirlem16  38663  poimirlem17  38664  poimirlem19  38666  poimirlem20  38667  poimirlem21  38668  poimirlem22  38669  poimirlem23  38670  poimirlem24  38671  poimirlem25  38672  poimirlem26  38673  poimirlem27  38674  poimirlem29  38676  poimirlem30  38677  poimirlem31  38678  poimirlem32  38679  itg2addnclem3  38700  ftc1anclem6  38725  dvasin  38731  unirep  38757  sdclem2  38785  ssbnd  38831  prdsbnd  38836  cntotbnd  38839  heibor1lem  38852  rrnequiv  38878  ismndo2  38917  grpoeqdivid  38924  isdrngo3  39002  crngohomfo  39049  0idl  39068  1idl  39069  divrngidl  39071  smprngopr  39095  prnc  39110  ispridlc  39113  disjimeceqim  39845  riotaclbgBAD  40120  lshpdisj  40153  lsateln0  40161  lsatcveq0  40198  opnlen0  40354  cmtbr4N  40421  cvrnbtwn2  40441  cvrnbtwn4  40445  atcvreq0  40480  cvlatexch1  40502  exatleN  40570  atlelt  40604  ps-2  40644  llnn0  40682  lplnn0N  40713  islpln2a  40714  lvoln0N  40757  islvol2aN  40758  4at  40779  dalemcea  40826  dalem3  40830  pmapglb2N  40937  pmapglb2xN  40938  cdlema1N  40957  cdlemb  40960  paddasslem17  41002  llnexchb2lem  41034  llnexchb2  41035  lhpat3  41212  ltrnid  41301  trlne  41351  cdlemc4  41360  cdleme11h  41432  cdlemednuN  41466  cdlemg1a  41736  tendoeq2  41940  tendoid0  41991  dva1dim  42151  dib1dim  42331  dihlatat  42503  dochkrshp4  42555  dochkr1  42644  lclkrlem2e  42677  lcfrlem16  42724  lcfrlem28  42736  mapd0  42831  hdmap14lem13  43046  eqresfnbd  43395  expeq1d  43490  expeqidd  43491  dvdsexpnn0  43495  reladdrsub  43545  sn-remul0ord  43568  sn-negex12  43577  sn-mullid  43596  sn-mul02  43625  nn0addcom  43635  nn0mulcom  43639  zmulcomlem  43640  mulgt0con1d  43643  mulgt0con2d  43644  sn-sup2  43664  frlmsnic  43713  evlselvlem  43725  prjspnnorm  43770  elrfi  43814  mrefg2  43827  eldiophb  43877  eldioph2b  43883  diophin  43892  diophun  43893  rexzrexnn0  43920  eldioph4b  43927  diophren  43929  rencldnfilem  43936  pellexlem6  43950  jm2.19  44109  rmydioph  44130  expdiophlem1  44137  expdioph  44139  lnr2i  44227  lpirlnr  44228  hbtlem2  44235  hbtlem4  44237  hbtlem6  44240  dgrsub2  44246  dgraa0p  44260  rngunsnply  44280  nlimsuc  44551  dfsucon  44633  radcnvrat  45407  pm14.24  45524  addrcom  45565  modelaxreplem1  46076  ormklocald  47994  afveu  48331  dfafn5b  48339  rlimdmafv  48355  afv2eu  48416  rlimdmafv2  48436  el1fzopredsuc  48504  minusmod5ne  48533  modmknepk  48546  elsetpreimafvssdm  48576  imasetpreimafvbijlemfo  48595  sprvalpw  48670  prprvalpw  48705  reupr  48712  fmtnofac2lem  48761  proththdlem  48806  perfectALTVlem2  48928  perfectALTV  48929  gbowpos  48965  gbowgt5  48968  gboge9  48970  nnsum4primesodd  49002  nnsum4primesoddALTV  49003  uhgrimedgi  49096  isuspgrim0  49100  isuspgrimlem  49101  upgrimpths  49115  clnbgrgrim  49140  grimedg  49141  grtrissvtx  49150  stgredgiun  49164  stgrvtx0  49168  isubgr3stgrlem7  49178  grlimgrtrilem2  49208  gpgiedgdmellem  49252  gpgvtxel2  49254  gpgvtx0  49259  gpgvtx1  49260  gpgusgralem  49262  gpgedgvtx0  49267  gpgedgvtx1  49268  gpgedg2ov  49272  gpgedg2iv  49273  gpgnbgrvtx0  49280  gpgnbgrvtx1  49281  pgnbgreunbgr  49331  ringcinvALTV  49515  smprngprmrng  49544  lincellss  49646  lindsrng01  49688  suppdm  49730  nnpw2pb  49807  0aryfvalel  49854  0aryfvalelfv  49855  itsclc0xyqsolr  49989  infsubc  50282  infsubc2  50283