Theorem syl5ibrcom 246

Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)

Hypotheses

Ref	Expression
syl5ibr.1	⊢ (𝜑 → 𝜃)
syl5ibr.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5ibrcom	⊢ (𝜑 → (𝜒 → 𝜓))

Proof of Theorem syl5ibrcom

Step	Hyp	Ref	Expression
1		syl5ibr.1	. . 3 ⊢ (𝜑 → 𝜃)
2		syl5ibr.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	syl5ibr 245	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
4	3	com12 32	1 ⊢ (𝜑 → (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimprcd  249  elsn2g  4610  preq1b  4790  elpreqprb  4811  reusv3  5345  alxfr  5347  reuhypd  5359  opth1  5414  euotd  5451  otiunsndisj  5458  tz7.2  5598  frsn  5699  dmopab2rex  5853  elsnxp  6223  reuop  6225  dfpo2  6228  ordtri1  6329  ordtri3  6332  fvmptdv2  6943  fveqressseq  7007  foco2  7033  fsn  7057  fnsnb  7088  fmptsng  7090  fmptsnd  7091  fconst2g  7128  fnprb  7134  fntpb  7135  funfvima  7156  soisoi  7249  isores3  7256  eqfunresadj  7281  riotaeqimp  7313  eusvobj2  7322  ovmpodv2  7485  f1opw2  7578  sorpssun  7637  sorpssin  7638  oneqmin  7705  nlimsucg  7748  onzsl  7752  tfinds  7766  funcnvuni  7838  opiota  7959  mposn  8003  suppssov1  8076  suppssfv  8080  brtpos  8113  frrlem12  8175  frrlem13  8176  wfrlem10OLD  8211  wfrlem14OLD  8215  wfrlem15OLD  8216  seqomlem1  8343  seqomlem2  8344  omordi  8460  omord  8462  omwordi  8465  oeeui  8496  nnmordi  8525  nnmord  8526  nnmwordi  8529  nnawordex  8531  nnaordex  8532  nneob  8549  omsmolem  8550  eldifsucnn  8557  qsss  8630  eroveu  8664  mapsncnv  8744  ralxpmap  8747  elixpsn  8788  ixpsnf1o  8789  boxcutc  8792  pw2f1olem  8933  2pwne  8990  mapxpen  9000  mapunen  9003  php  9067  phpOLD  9079  onomeneq  9085  unxpdomlem2  9108  en1eqsnbi  9133  isfiniteg  9161  fofinf1o  9184  f1opwfi  9213  elfiun  9279  oieu  9388  brwdom2  9422  wdomtr  9424  ixpiunwdom  9439  en3lplem1  9461  suc11reg  9468  inf3lemd  9476  cantnfvalf  9514  cantnflt  9521  cantnfp1lem3  9529  cantnflem2  9539  ttrcltr  9565  rnttrcl  9571  ttrclselem1  9574  r1tr  9625  updjud  9783  dfac8alem  9878  wdomnumr  9913  isinfcard  9941  aceq3lem  9969  dfac5lem4  9975  dfac5  9977  dfac2b  9979  coftr  10122  fin23lem28  10189  fin23lem29  10190  fin1a2lem11  10259  fin1a2lem12  10260  fin1a2lem13  10261  hsmexlem9  10274  axdclem  10368  pwcfsdom  10432  gchdomtri  10478  fpwwe2  10492  gchpwdom  10519  gchhar  10528  addnidpi  10750  nqereu  10778  genpv  10848  genpdm  10851  distrlem5pr  10876  mulid1  11066  ltne  11165  mul02  11246  cnegex  11249  mul0or  11708  negfi  12017  sup2  12024  supaddc  12035  supadd  12036  supmul1  12037  supmul  12040  creur  12060  creui  12061  cju  12062  nnsub  12110  un0addcl  12359  un0mulcl  12360  nn0sub  12376  elz2  12430  zaddcl  12453  suprzcl2  12771  qmulz  12784  qre  12786  qnegcl  12799  elpqb  12809  xrmax1  13002  xrmin2  13005  max1ALT  13013  xlesubadd  13090  xmulass  13114  xlemul1a  13115  xrsupexmnf  13132  xrinfmexpnf  13133  xrub  13139  iccid  13217  fzsn  13391  fzsuc2  13407  fz1sbc  13425  elfzp12  13428  modmuladd  13726  seqid3  13860  bcval5  14125  bcpasc  14128  hashbnd  14143  hashnnn0genn0  14150  hashprg  14202  hashfzo  14236  wrdl1s1  14410  ccats1alpha  14415  cats1un  14524  shftlem  14870  replim  14918  absmod0  15106  absz  15114  rlimdm  15351  summolem2  15519  summo  15520  zsum  15521  fsum  15523  fsummulc2  15587  fsumconst  15593  fsum00  15601  incexclem  15639  isumsplit  15643  infcvgaux1i  15660  prodmolem2  15736  prodmo  15737  zprod  15738  fprod  15742  prodsn  15763  prodsnf  15765  fprodconst  15779  ruclem2  16032  fzo0dvdseq  16123  bitsf1ocnv  16242  sadcaddlem  16255  smueqlem  16288  gcdabs1  16327  bezoutlem1  16338  bezoutlem3  16340  bezoutlem4  16341  dvdsgcd  16343  dvdsmulgcd  16354  lcmgcdeq  16406  lcmf  16427  lcmfunsnlem1  16431  lcmfunsnlem2lem2  16433  isprm2lem  16475  dvdsprime  16481  isprm5  16501  coprm  16505  prmdvdsexpr  16511  rpexp  16516  phibndlem  16560  dfphi2  16564  hashgcdlem  16578  odzdvds  16585  nnoddn2prm  16601  pythagtriplem1  16606  iserodd  16625  pceulem  16635  pcqmul  16643  pcqcl  16646  pcxnn0cl  16650  pcxcl  16651  pcneg  16664  pcabs  16665  pcgcd1  16667  pcz  16671  pcprmpw2  16672  pcprmpw  16673  dvdsprmpweqle  16676  difsqpwdvds  16677  pcaddlem  16678  pcadd  16679  pcmpt  16682  pockthg  16696  prmreclem5  16710  4sqlem4  16742  mul4sq  16744  vdwapun  16764  vdwlem2  16772  vdwlem6  16776  vdwlem8  16778  vdwlem13  16783  0ram  16810  ram0  16812  ramcl  16819  cshwsiun  16890  wunress  17049  wunressOLD  17050  firest  17232  isssc  17621  pospo  18152  latnlej  18263  gsumval2a  18458  mnd1id  18516  0subm  18545  mulgnn0p1  18803  mulgnn0ass  18827  cyccom  18910  gicsubgen  18982  symg1bas  19086  snsymgefmndeq  19090  psgnunilem1  19189  psgnunilem2  19191  mndodcongi  19239  oddvdsnn0  19240  odnncl  19241  oddvds  19243  odeq  19246  odeq1  19255  pgpfi2  19299  sylow2a  19312  sylow2blem3  19315  sylow3lem6  19325  lsmelvalm  19344  lsmsubm  19346  lsmsubg  19347  lsmmod  19368  lsmdisj2  19375  efgmnvl  19407  efgtlen  19419  efgs1b  19429  efgrelexlemb  19443  efgredeu  19445  efgcpbllemb  19448  frgpuptinv  19464  frgpup3lem  19470  qusabl  19553  frgpnabllem1  19561  cyggeninv  19570  cyggenod  19571  cygablOLD  19579  gsumval3eu  19592  dprdssv  19706  dprdfeq0  19712  dprdsubg  19714  dprddisj2  19729  ablfacrp  19756  pgpfac1lem3  19767  pgpfaclem2  19772  dvreq1  20022  irredn1  20035  drngmul0or  20109  isabvd  20178  abvdom  20196  issrngd  20219  lmodfopnelem2  20258  lss1d  20323  lspsneq0  20372  lbspss  20442  lsmcl  20443  lvecvs0or  20468  lspindpi  20492  lidl1el  20587  lpiss  20619  lidldvgen  20624  nzrunit  20636  rrgeq0  20659  domneq0  20666  qsssubdrg  20755  zringlpirlem1  20782  znfld  20866  znunit  20869  znrrg  20871  cygznlem3  20875  frgpcyg  20879  psgnghm  20883  ipeq0  20941  cssincl  20991  lsmcss  20995  obselocv  21033  dsmmacl  21046  dsmmlss  21049  mplsubrglem  21308  mplmonmul  21335  mplcoe5lem  21338  mhpsclcl  21435  mhpvarcl  21436  coe1tmmul2  21545  coe1tmmul  21546  pf1ind  21619  mat1dimelbas  21718  mdetralt  21855  mdetunilem2  21860  mdetunilem7  21865  mdetunilem9  21867  maducoeval2  21887  chpscmat  22089  chfacfscmulgsum  22107  chfacfpmmulgsum  22111  istopon  22159  eltg3  22210  tgidm  22228  clsval2  22299  opncldf1  22333  restbas  22407  tgrest  22408  restcld  22421  restcldr  22423  restcls  22430  restntr  22431  ordtbas2  22440  ordtbas  22441  ordtrest2lem  22452  ordtrest2  22453  pnfnei  22469  mnfnei  22470  tgcn  22501  cnconst  22533  cnindis  22541  lmss  22547  ordtt1  22628  discmp  22647  1stcrest  22702  2ndcdisj  22705  cldllycmp  22744  txbas  22816  ptpjpre1  22820  ptuni2  22825  ptbasin  22826  ptbasfi  22830  ptopn2  22833  txbasval  22855  ptpjopn  22861  ptclsg  22864  dfac14lem  22866  xkoccn  22868  ptcnp  22871  upxp  22872  ptrescn  22888  txkgen  22901  xkoptsub  22903  xkopt  22904  xkoco1cn  22906  xkoco2cn  22907  xkococn  22909  xkoinjcn  22936  ordthmeolem  23050  ptuncnv  23056  nrmhaus  23075  fbssint  23087  fbfinnfr  23090  fbasrn  23133  isufil2  23157  filufint  23169  rnelfm  23202  fmfnfmlem2  23204  fmfnfmlem3  23205  fmfnfmlem4  23206  fmfnfm  23207  flimtopon  23219  flimclslem  23233  fclstopon  23261  fclscf  23274  flimfnfcls  23277  alexsublem  23293  alexsubALTlem3  23298  alexsubALTlem4  23299  ptcmplem2  23302  tmdgsum2  23345  symgtgp  23355  cldsubg  23360  qustgplem  23370  tgptsmscld  23400  tsmsxplem1  23402  imasdsf1olem  23624  blssps  23675  blss  23676  stdbdxmet  23769  methaus  23774  metrest  23778  nrginvrcn  23954  nmoeq0  23998  blssioo  24056  xrtgioo  24067  xrsxmet  24070  reconnlem1  24087  reconnlem2  24088  xrge0tsms  24095  elcncf1di  24156  iccpnfcnv  24205  evth  24220  lebnumlem1  24222  lebnumlem2  24223  lebnumlem3  24224  nmoleub3  24380  minveclem3b  24690  ivthlem2  24714  ivthlem3  24715  elovolm  24737  ovolmge0  24739  ovoliun  24767  ovolicc2lem3  24781  ovolicc2  24784  voliunlem3  24814  dyaddisj  24858  dyadmax  24860  opnmblALT  24865  ismbfd  24901  ismbf2d  24902  mbfimaopnlem  24917  mbfimaopn2  24919  i1fmullem  24956  i1fres  24968  itg1climres  24977  mbfi1fseqlem4  24981  itg2lcl  24990  itgsplitioo  25100  ellimc2  25139  rolle  25252  dvlip  25255  dvge0  25268  dvne0  25273  lhop1lem  25275  tdeglem4  25322  tdeglem4OLD  25323  degltlem1  25335  deg1nn0clb  25353  deg1lt0  25354  dvdsq1p  25423  ply1rem  25426  fta1g  25430  elply2  25455  plyf  25457  ne0p  25466  plyeq0lem  25469  plypf1  25471  0dgrb  25505  coe1termlem  25517  dgrcolem2  25533  plymul0or  25539  plyrem  25563  fta1  25566  quotcan  25567  aalioulem3  25592  eff1olem  25802  lognegb  25843  eflogeq  25855  argregt0  25863  argrege0  25864  tanarg  25872  cxpexp  25921  cxpeq0  25931  mulcxp  25938  cxpeq  26008  atans2  26179  scvxcvx  26233  dmgmaddn0  26270  isppw2  26362  vmappw  26363  vmacl  26365  efvmacl  26367  isnsqf  26382  mumullem2  26427  sqff1o  26429  dvdsppwf1o  26433  ppiublem1  26448  vmalelog  26451  chtublem  26457  fsumvma  26459  perfectlem2  26476  perfect  26477  bposlem1  26530  lgsmod  26569  lgsne0  26581  lgsdirnn0  26590  lgsqr  26597  lgsdchr  26601  gausslemma2dlem1a  26611  gausslemma2dlem6  26618  lgseisenlem2  26622  lgsquadlem1  26626  lgsquadlem2  26627  2lgslem1b  26638  2sqlem2  26664  mul2sq  26665  2sqlem7  26670  dchrisum0fno1  26757  pntrsumbnd2  26813  ostthlem1  26873  ostth2lem2  26880  ostth3  26884  ostth  26885  nolesgn2ores  26918  nogesgn1ores  26920  nolt02o  26941  nogt01o  26942  nosupbnd2  26962  noinfbnd2lem1  26976  noetasuplem4  26982  noetainflem4  26986  colinearalg  27508  axpasch  27539  axlowdimlem16  27555  axlowdimlem17  27556  axlowdim  27559  axcontlem2  27563  axcontlem4  27565  axcontlem7  27568  lpvtx  27668  edglnl  27743  numedglnl  27744  usgredgop  27770  usgrexmplef  27856  uhgrspansubgrlem  27887  uhgrspan1  27900  nbusgredgeu0  27965  nb3grprlem2  27978  cusgrsize2inds  28050  vtxd0nedgb  28085  rusgrpropnb  28180  upgrwlkvtxedg  28242  wlkp1lem1  28270  wlkp1lem6  28275  wlkp1lem8  28277  usgr2wlkneq  28353  crctcshwlk  28416  crctcsh  28418  iswwlksnon  28447  wlkiswwlks1  28461  wwlksnextbi  28488  wwlksnextproplem2  28504  wspthsnonn0vne  28511  clwlkclwwlklem2  28593  clwwisshclwws  28608  erclwwlktr  28615  clwwlkel  28639  clwwlkext2edg  28649  erclwwlkntr  28664  clwlknf1oclwwlknlem2  28675  clwlknf1oclwwlknlem3  28676  clwlknf1oclwwlkn  28677  clwwlknonccat  28689  0wlkons1  28714  3wlkdlem6  28758  eupth2eucrct  28810  frgrwopreglem2  28906  2clwwlk2clwwlk  28943  wlkl0  28960  nvmul0or  29241  ipasslem5  29426  ipasslem11  29431  hvmul0or  29616  his6  29690  hhssnv  29855  ocsh  29874  ocin  29887  shsidmi  29975  chnlen0  30035  h1de2bi  30145  h1de2ctlem  30146  h1de2ci  30147  spansni  30148  3oalem1  30253  nmcexi  30617  atcveq0  30939  chcv1  30946  cdjreui  31023  cdj3lem2b  31028  xrge0tsmsd  31545  1fldgenq  31734  ccfldextdgrr  31981  ordtrest2NEWlem  32111  ordtrest2NEW  32112  xrge0iifcnv  32122  esumc  32258  esumpcvgval  32285  ballotlemfc0  32700  ballotlemfcc  32701  subfacp1lem4  33385  subfacp1lem5  33386  erdszelem8  33400  sconnpi1  33441  cvmsss2  33476  cvmlift2lem12  33516  satfv0  33560  satfv0fun  33573  satf00  33576  sat1el2xp  33581  fmla0xp  33585  fmlasucdisj  33601  satffunlem1lem1  33604  satffunlem2lem1  33606  dmopab3rexdif  33607  msubco  33733  msubvrs  33762  sinccvglem  33870  untsucf  33891  nnuni  33926  dfrdg2  33998  frpoins3xpg  34013  frpoins3xp3g  34014  poxp2  34016  xpord2pred  34018  sexp2  34019  poxp3  34022  xpord3pred  34024  madef  34131  sltlpss  34178  lrrecfr  34191  addsval  34217  colineardim1  34454  btwnconn1lem14  34493  segleantisym  34508  colinbtwnle  34511  outsidele  34525  lineunray  34540  linethru  34546  elicc3  34597  opnregcld  34610  cldregopn  34611  fnejoin2  34649  bj-isrvec  35563  dissneqlem  35609  icorempo  35620  relowlssretop  35632  relowlpssretop  35633  rdgssun  35647  finxpsuclem  35666  lindsenlbs  35870  ptrecube  35875  poimirlem6  35881  poimirlem7  35882  poimirlem16  35891  poimirlem17  35892  poimirlem19  35894  poimirlem20  35895  poimirlem21  35896  poimirlem22  35897  poimirlem23  35898  poimirlem24  35899  poimirlem25  35900  poimirlem26  35901  poimirlem27  35902  poimirlem29  35904  poimirlem30  35905  poimirlem31  35906  poimirlem32  35907  itg2addnclem3  35928  ftc1anclem6  35953  dvasin  35959  unirep  35969  sdclem2  35998  ssbnd  36044  prdsbnd  36049  cntotbnd  36052  heibor1lem  36065  rrnequiv  36091  ismndo2  36130  grpoeqdivid  36137  isdrngo3  36215  crngohomfo  36262  0idl  36281  1idl  36282  divrngidl  36284  smprngopr  36308  prnc  36323  ispridlc  36326  riotaclbgBAD  37214  lshpdisj  37247  lsateln0  37255  lsatcveq0  37292  opnlen0  37448  cmtbr4N  37515  cvrnbtwn2  37535  cvrnbtwn4  37539  atcvreq0  37574  cvlatexch1  37596  exatleN  37665  atlelt  37699  ps-2  37739  llnn0  37777  lplnn0N  37808  islpln2a  37809  lvoln0N  37852  islvol2aN  37853  4at  37874  dalemcea  37921  dalem3  37925  pmapglb2N  38032  pmapglb2xN  38033  cdlema1N  38052  cdlemb  38055  paddasslem17  38097  llnexchb2lem  38129  llnexchb2  38130  lhpat3  38307  ltrnid  38396  trlne  38446  cdlemc4  38455  cdleme11h  38527  cdlemednuN  38561  cdlemg1a  38831  tendoeq2  39035  tendoid0  39086  dva1dim  39246  dib1dim  39426  dihlatat  39598  dochkrshp4  39650  dochkr1  39739  lclkrlem2e  39772  lcfrlem16  39819  lcfrlem28  39831  mapd0  39926  hdmap14lem13  40141  fnsnbt  40453  frlmsnic  40513  dvdsexpnn0  40591  reladdrsub  40618  sn-negex12  40648  sn-mulid2  40667  sn-mul02  40672  mulgt0con1d  40678  mulgt0con2d  40679  sn-sup2  40689  prjspner1  40713  prjcrv0  40720  elrfi  40766  mrefg2  40779  eldiophb  40829  eldioph2b  40835  diophin  40844  diophun  40845  rexzrexnn0  40876  eldioph4b  40883  diophren  40885  rencldnfilem  40892  pellexlem6  40906  jm2.19  41066  rmydioph  41087  expdiophlem1  41094  expdioph  41096  lnr2i  41192  lpirlnr  41193  hbtlem2  41200  hbtlem4  41202  hbtlem6  41205  dgrsub2  41211  dgraa0p  41225  rngunsnply  41249  nlimsuc  41358  dfsucon  41440  radcnvrat  42242  pm14.24  42360  addrcom  42403  afveu  44985  dfafn5b  44993  rlimdmafv  45009  afv2eu  45070  rlimdmafv2  45090  el1fzopredsuc  45157  elsetpreimafvssdm  45178  imasetpreimafvbijlemfo  45197  sprvalpw  45272  prprvalpw  45307  reupr  45314  fmtnofac2lem  45360  proththdlem  45405  perfectALTVlem2  45514  perfectALTV  45515  gbowpos  45551  gbowgt5  45554  gboge9  45556  nnsum4primesodd  45588  nnsum4primesoddALTV  45589  isomuspgr  45626  ringcinv  45930  ringcinvALTV  45954  lincellss  46107  lindsrng01  46149  suppdm  46191  nnpw2pb  46273  0aryfvalel  46320  0aryfvalelfv  46321  itsclc0xyqsolr  46455  natlocalincr  46851