Theorem syl5ibrcom 250

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  biimprcd  253  elsn2g  4569  preq1b  4747  elpreqprb  4768  reusv3  5287  alxfr  5289  reuhypd  5301  opth1  5348  euotd  5385  otiunsndisj  5392  tz7.2  5524  frsn  5625  dmopab2rex  5775  elsnxp  6143  reuop  6145  ordtri1  6235  ordtri3  6238  fvmptdv2  6825  fveqressseq  6889  foco2  6915  fsn  6939  fnsnb  6970  fmptsng  6972  fmptsnd  6973  fconst2g  7007  fnprb  7013  fntpb  7014  funfvima  7035  soisoi  7126  isores3  7133  riotaeqimp  7186  eusvobj2  7195  ovmpodv2  7356  f1opw2  7449  sorpssun  7507  sorpssin  7508  oneqmin  7573  nlimsucg  7610  onzsl  7614  tfinds  7627  funcnvuni  7698  opiota  7818  mposn  7860  suppssov1  7929  suppssfv  7933  brtpos  7966  frrlem12  8027  frrlem13  8028  wfrlem10  8053  wfrlem14  8057  wfrlem15  8058  seqomlem1  8175  seqomlem2  8176  omordi  8283  omord  8285  omwordi  8288  oeeui  8319  nnmordi  8348  nnmord  8349  nnmwordi  8352  nnawordex  8354  nnaordex  8355  nneob  8370  omsmolem  8371  qsss  8449  eroveu  8483  mapsncnv  8563  ralxpmap  8566  elixpsn  8607  ixpsnf1o  8608  boxcutc  8611  pw2f1olem  8738  2pwne  8791  mapxpen  8801  mapunen  8804  php  8819  unxpdomlem2  8872  en1eqsnbi  8894  isfiniteg  8920  fofinf1o  8940  f1opwfi  8969  elfiun  9035  oieu  9144  brwdom2  9178  wdomtr  9180  ixpiunwdom  9195  en3lplem1  9216  suc11reg  9223  inf3lemd  9231  cantnfvalf  9269  cantnflt  9276  cantnfp1lem3  9284  cantnflem2  9294  trpred0  9326  r1tr  9375  updjud  9533  dfac8alem  9626  wdomnumr  9661  isinfcard  9689  aceq3lem  9717  dfac5lem4  9723  dfac5  9725  dfac2b  9727  coftr  9870  fin23lem28  9937  fin23lem29  9938  fin1a2lem11  10007  fin1a2lem12  10008  fin1a2lem13  10009  hsmexlem9  10022  axdclem  10116  pwcfsdom  10180  gchdomtri  10226  fpwwe2  10240  gchpwdom  10267  gchhar  10276  addnidpi  10498  nqereu  10526  genpv  10596  genpdm  10599  distrlem5pr  10624  mulid1  10814  ltne  10912  mul02  10993  cnegex  10996  mul0or  11455  negfi  11764  sup2  11771  supaddc  11782  supadd  11783  supmul1  11784  supmul  11787  creur  11807  creui  11808  cju  11809  nnsub  11857  un0addcl  12106  un0mulcl  12107  nn0sub  12123  elz2  12177  zaddcl  12200  suprzcl2  12517  qmulz  12530  qre  12532  qnegcl  12545  elpqb  12555  xrmax1  12748  xrmin2  12751  max1ALT  12759  xlesubadd  12836  xmulass  12860  xlemul1a  12861  xrsupexmnf  12878  xrinfmexpnf  12879  xrub  12885  iccid  12963  fzsn  13137  fzsuc2  13153  fz1sbc  13171  elfzp12  13174  modmuladd  13469  seqid3  13603  bcval5  13867  bcpasc  13870  hashbnd  13885  hashnnn0genn0  13892  hashprg  13945  hashfzo  13979  wrdl1s1  14154  ccats1alpha  14159  cats1un  14269  shftlem  14614  replim  14662  absmod0  14850  absz  14858  rlimdm  15095  summolem2  15263  summo  15264  zsum  15265  fsum  15267  fsummulc2  15329  fsumconst  15335  fsum00  15343  incexclem  15381  isumsplit  15385  infcvgaux1i  15402  prodmolem2  15478  prodmo  15479  zprod  15480  fprod  15484  prodsn  15505  prodsnf  15507  fprodconst  15521  ruclem2  15774  fzo0dvdseq  15865  bitsf1ocnv  15984  sadcaddlem  15997  smueqlem  16030  gcdabs1  16069  bezoutlem1  16080  bezoutlem3  16082  bezoutlem4  16083  dvdsgcd  16085  dvdsmulgcd  16098  lcmgcdeq  16150  lcmf  16171  lcmfunsnlem1  16175  lcmfunsnlem2lem2  16177  isprm2lem  16219  dvdsprime  16225  isprm5  16245  coprm  16249  prmdvdsexpr  16255  rpexp  16260  phibndlem  16304  dfphi2  16308  hashgcdlem  16322  odzdvds  16329  nnoddn2prm  16345  pythagtriplem1  16350  iserodd  16369  pceulem  16379  pcqmul  16387  pcqcl  16390  pcxnn0cl  16394  pcxcl  16395  pcneg  16408  pcabs  16409  pcgcd1  16411  pcz  16415  pcprmpw2  16416  pcprmpw  16417  dvdsprmpweqle  16420  difsqpwdvds  16421  pcaddlem  16422  pcadd  16423  pcmpt  16426  pockthg  16440  prmreclem5  16454  4sqlem4  16486  mul4sq  16488  vdwapun  16508  vdwlem2  16516  vdwlem6  16520  vdwlem8  16522  vdwlem13  16527  0ram  16554  ram0  16556  ramcl  16563  cshwsiun  16634  wunress  16766  firest  16909  isssc  17297  pospo  17823  latnlej  17934  gsumval2a  18129  mnd1id  18187  0subm  18216  mulgnn0p1  18475  mulgnn0ass  18499  cyccom  18582  gicsubgen  18654  symg1bas  18755  snsymgefmndeq  18759  psgnunilem1  18857  psgnunilem2  18859  mndodcongi  18907  oddvdsnn0  18908  odnncl  18909  oddvds  18911  odeq  18914  odeq1  18923  pgpfi2  18967  sylow2a  18980  sylow2blem3  18983  sylow3lem6  18993  lsmelvalm  19012  lsmsubm  19014  lsmsubg  19015  lsmmod  19037  lsmdisj2  19044  efgmnvl  19076  efgtlen  19088  efgs1b  19098  efgrelexlemb  19112  efgredeu  19114  efgcpbllemb  19117  frgpuptinv  19133  frgpup3lem  19139  qusabl  19222  frgpnabllem1  19230  cyggeninv  19239  cyggenod  19240  cygablOLD  19248  gsumval3eu  19261  dprdssv  19375  dprdfeq0  19381  dprdsubg  19383  dprddisj2  19398  ablfacrp  19425  pgpfac1lem3  19436  pgpfaclem2  19441  dvreq1  19683  irredn1  19696  drngmul0or  19760  isabvd  19828  abvdom  19846  issrngd  19869  lmodfopnelem2  19908  lss1d  19972  lspsneq0  20021  lbspss  20091  lsmcl  20092  lvecvs0or  20117  lspindpi  20141  lidl1el  20228  lpiss  20260  lidldvgen  20265  nzrunit  20277  rrgeq0  20300  domneq0  20307  qsssubdrg  20394  zringlpirlem1  20421  znfld  20497  znunit  20500  znrrg  20502  cygznlem3  20506  frgpcyg  20510  psgnghm  20514  ipeq0  20572  cssincl  20622  lsmcss  20626  obselocv  20662  dsmmacl  20675  dsmmlss  20678  mplsubrglem  20938  mplmonmul  20965  mplcoe5lem  20968  mhpsclcl  21059  mhpvarcl  21060  coe1tmmul2  21169  coe1tmmul  21170  pf1ind  21243  mat1dimelbas  21340  mdetralt  21477  mdetunilem2  21482  mdetunilem7  21487  mdetunilem9  21489  maducoeval2  21509  chpscmat  21711  chfacfscmulgsum  21729  chfacfpmmulgsum  21733  istopon  21781  eltg3  21831  tgidm  21849  clsval2  21919  opncldf1  21953  restbas  22027  tgrest  22028  restcld  22041  restcldr  22043  restcls  22050  restntr  22051  ordtbas2  22060  ordtbas  22061  ordtrest2lem  22072  ordtrest2  22073  pnfnei  22089  mnfnei  22090  tgcn  22121  cnconst  22153  cnindis  22161  lmss  22167  ordtt1  22248  discmp  22267  1stcrest  22322  2ndcdisj  22325  cldllycmp  22364  txbas  22436  ptpjpre1  22440  ptuni2  22445  ptbasin  22446  ptbasfi  22450  ptopn2  22453  txbasval  22475  ptpjopn  22481  ptclsg  22484  dfac14lem  22486  xkoccn  22488  ptcnp  22491  upxp  22492  ptrescn  22508  txkgen  22521  xkoptsub  22523  xkopt  22524  xkoco1cn  22526  xkoco2cn  22527  xkococn  22529  xkoinjcn  22556  ordthmeolem  22670  ptuncnv  22676  nrmhaus  22695  fbssint  22707  fbfinnfr  22710  fbasrn  22753  isufil2  22777  filufint  22789  rnelfm  22822  fmfnfmlem2  22824  fmfnfmlem3  22825  fmfnfmlem4  22826  fmfnfm  22827  flimtopon  22839  flimclslem  22853  fclstopon  22881  fclscf  22894  flimfnfcls  22897  alexsublem  22913  alexsubALTlem3  22918  alexsubALTlem4  22919  ptcmplem2  22922  tmdgsum2  22965  symgtgp  22975  cldsubg  22980  qustgplem  22990  tgptsmscld  23020  tsmsxplem1  23022  imasdsf1olem  23243  blssps  23294  blss  23295  stdbdxmet  23385  methaus  23390  metrest  23394  nrginvrcn  23562  nmoeq0  23606  blssioo  23664  xrtgioo  23675  xrsxmet  23678  reconnlem1  23695  reconnlem2  23696  xrge0tsms  23703  elcncf1di  23764  iccpnfcnv  23813  evth  23828  lebnumlem1  23830  lebnumlem2  23831  lebnumlem3  23832  nmoleub3  23988  minveclem3b  24297  ivthlem2  24321  ivthlem3  24322  elovolm  24344  ovolmge0  24346  ovoliun  24374  ovolicc2lem3  24388  ovolicc2  24391  voliunlem3  24421  dyaddisj  24465  dyadmax  24467  opnmblALT  24472  ismbfd  24508  ismbf2d  24509  mbfimaopnlem  24524  mbfimaopn2  24526  i1fmullem  24563  i1fres  24575  itg1climres  24584  mbfi1fseqlem4  24588  itg2lcl  24597  itgsplitioo  24707  ellimc2  24746  rolle  24859  dvlip  24862  dvge0  24875  dvne0  24880  lhop1lem  24882  tdeglem4  24929  tdeglem4OLD  24930  degltlem1  24942  deg1nn0clb  24960  deg1lt0  24961  dvdsq1p  25030  ply1rem  25033  fta1g  25037  elply2  25062  plyf  25064  ne0p  25073  plyeq0lem  25076  plypf1  25078  0dgrb  25112  coe1termlem  25124  dgrcolem2  25140  plymul0or  25146  plyrem  25170  fta1  25173  quotcan  25174  aalioulem3  25199  eff1olem  25409  lognegb  25450  eflogeq  25462  argregt0  25470  argrege0  25471  tanarg  25479  cxpexp  25528  cxpeq0  25538  mulcxp  25545  cxpeq  25615  atans2  25786  scvxcvx  25840  dmgmaddn0  25877  isppw2  25969  vmappw  25970  vmacl  25972  efvmacl  25974  isnsqf  25989  mumullem2  26034  sqff1o  26036  dvdsppwf1o  26040  ppiublem1  26055  vmalelog  26058  chtublem  26064  fsumvma  26066  perfectlem2  26083  perfect  26084  bposlem1  26137  lgsmod  26176  lgsne0  26188  lgsdirnn0  26197  lgsqr  26204  lgsdchr  26208  gausslemma2dlem1a  26218  gausslemma2dlem6  26225  lgseisenlem2  26229  lgsquadlem1  26233  lgsquadlem2  26234  2lgslem1b  26245  2sqlem2  26271  mul2sq  26272  2sqlem7  26277  dchrisum0fno1  26364  pntrsumbnd2  26420  ostthlem1  26480  ostth2lem2  26487  ostth3  26491  ostth  26492  colinearalg  26973  axpasch  27004  axlowdimlem16  27020  axlowdimlem17  27021  axlowdim  27024  axcontlem2  27028  axcontlem4  27030  axcontlem7  27033  lpvtx  27131  edglnl  27206  numedglnl  27207  usgredgop  27233  usgrexmplef  27319  uhgrspansubgrlem  27350  uhgrspan1  27363  nbusgredgeu0  27428  nb3grprlem2  27441  cusgrsize2inds  27513  vtxd0nedgb  27548  rusgrpropnb  27643  upgrwlkvtxedg  27704  wlkp1lem1  27733  wlkp1lem6  27738  wlkp1lem8  27740  usgr2wlkneq  27815  crctcshwlk  27878  crctcsh  27880  iswwlksnon  27909  wlkiswwlks1  27923  wwlksnextbi  27950  wwlksnextproplem2  27966  wspthsnonn0vne  27973  clwlkclwwlklem2  28055  clwwisshclwws  28070  erclwwlktr  28077  clwwlkel  28101  clwwlkext2edg  28111  erclwwlkntr  28126  clwlknf1oclwwlknlem2  28137  clwlknf1oclwwlknlem3  28138  clwlknf1oclwwlkn  28139  clwwlknonccat  28151  0wlkons1  28176  3wlkdlem6  28220  eupth2eucrct  28272  frgrwopreglem2  28368  2clwwlk2clwwlk  28405  wlkl0  28422  nvmul0or  28703  ipasslem5  28888  ipasslem11  28893  hvmul0or  29078  his6  29152  hhssnv  29317  ocsh  29336  ocin  29349  shsidmi  29437  chnlen0  29497  h1de2bi  29607  h1de2ctlem  29608  h1de2ci  29609  spansni  29610  3oalem1  29715  nmcexi  30079  atcveq0  30401  chcv1  30408  cdjreui  30485  cdj3lem2b  30490  xrge0tsmsd  31008  ccfldextdgrr  31428  ordtrest2NEWlem  31558  ordtrest2NEW  31559  xrge0iifcnv  31569  esumc  31703  esumpcvgval  31730  ballotlemfc0  32143  ballotlemfcc  32144  subfacp1lem4  32830  subfacp1lem5  32831  erdszelem8  32845  sconnpi1  32886  cvmsss2  32921  cvmlift2lem12  32961  satfv0  33005  satfv0fun  33018  satf00  33021  sat1el2xp  33026  fmla0xp  33030  fmlasucdisj  33046  satffunlem1lem1  33049  satffunlem2lem1  33051  dmopab3rexdif  33052  msubco  33178  msubvrs  33207  sinccvglem  33315  untsucf  33336  dfpo2  33410  eqfunresadj  33423  dfrdg2  33459  frpoins3xpg  33475  frpoins3xp3g  33476  poxp2  33478  xpord2pred  33480  sexp2  33481  poxp3  33484  xpord3pred  33486  nolesgn2ores  33569  nogesgn1ores  33571  nolt02o  33592  nogt01o  33593  nosupbnd2  33613  noinfbnd2lem1  33627  noetasuplem4  33633  noetainflem4  33637  madef  33734  sltlpss  33781  lrrecfr  33794  addsval  33820  colineardim1  34057  btwnconn1lem14  34096  segleantisym  34111  colinbtwnle  34114  outsidele  34128  lineunray  34143  linethru  34149  elicc3  34200  opnregcld  34213  cldregopn  34214  fnejoin2  34252  dissneqlem  35205  icorempo  35216  relowlssretop  35228  relowlpssretop  35229  rdgssun  35243  finxpsuclem  35262  lindsenlbs  35466  ptrecube  35471  poimirlem6  35477  poimirlem7  35478  poimirlem16  35487  poimirlem17  35488  poimirlem19  35490  poimirlem20  35491  poimirlem21  35492  poimirlem22  35493  poimirlem23  35494  poimirlem24  35495  poimirlem25  35496  poimirlem26  35497  poimirlem27  35498  poimirlem29  35500  poimirlem30  35501  poimirlem31  35502  poimirlem32  35503  itg2addnclem3  35524  ftc1anclem6  35549  dvasin  35555  unirep  35565  sdclem2  35594  ssbnd  35640  prdsbnd  35645  cntotbnd  35648  heibor1lem  35661  rrnequiv  35687  ismndo2  35726  grpoeqdivid  35733  isdrngo3  35811  crngohomfo  35858  0idl  35877  1idl  35878  divrngidl  35880  smprngopr  35904  prnc  35919  ispridlc  35922  riotaclbgBAD  36662  lshpdisj  36695  lsateln0  36703  lsatcveq0  36740  opnlen0  36896  cmtbr4N  36963  cvrnbtwn2  36983  cvrnbtwn4  36987  atcvreq0  37022  cvlatexch1  37044  exatleN  37112  atlelt  37146  ps-2  37186  llnn0  37224  lplnn0N  37255  islpln2a  37256  lvoln0N  37299  islvol2aN  37300  4at  37321  dalemcea  37368  dalem3  37372  pmapglb2N  37479  pmapglb2xN  37480  cdlema1N  37499  cdlemb  37502  paddasslem17  37544  llnexchb2lem  37576  llnexchb2  37577  lhpat3  37754  ltrnid  37843  trlne  37893  cdlemc4  37902  cdleme11h  37974  cdlemednuN  38008  cdlemg1a  38278  tendoeq2  38482  tendoid0  38533  dva1dim  38693  dib1dim  38873  dihlatat  39045  dochkrshp4  39097  dochkr1  39186  lclkrlem2e  39219  lcfrlem16  39266  lcfrlem28  39278  mapd0  39373  hdmap14lem13  39588  fnsnbt  39873  frlmsnic  39927  dvdsexpnn0  40001  reladdrsub  40028  sn-negex12  40058  sn-mulid2  40077  sn-mul02  40082  mulgt0con1d  40088  mulgt0con2d  40089  sn-sup2  40099  prjspner1  40123  elrfi  40171  mrefg2  40184  eldiophb  40234  eldioph2b  40240  diophin  40249  diophun  40250  rexzrexnn0  40281  eldioph4b  40288  diophren  40290  rencldnfilem  40297  pellexlem6  40311  jm2.19  40470  rmydioph  40491  expdiophlem1  40498  expdioph  40500  lnr2i  40596  lpirlnr  40597  hbtlem2  40604  hbtlem4  40606  hbtlem6  40609  dgrsub2  40615  dgraa0p  40629  rngunsnply  40653  dfsucon  40767  radcnvrat  41557  pm14.24  41675  addrcom  41718  afveu  44271  dfafn5b  44279  rlimdmafv  44295  afv2eu  44356  rlimdmafv2  44376  el1fzopredsuc  44444  elsetpreimafvssdm  44465  imasetpreimafvbijlemfo  44484  sprvalpw  44559  prprvalpw  44594  reupr  44601  fmtnofac2lem  44647  proththdlem  44692  perfectALTVlem2  44801  perfectALTV  44802  gbowpos  44838  gbowgt5  44841  gboge9  44843  nnsum4primesodd  44875  nnsum4primesoddALTV  44876  isomuspgr  44913  lincellss  45394  lindsrng01  45436  suppdm  45478  nnpw2pb  45560  0aryfvalel  45607  0aryfvalelfv  45608  itsclc0xyqsolr  45742