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  4600  preq1b  4778  elpreqprb  4799  reusv3  5329  alxfr  5331  reuhypd  5343  opth1  5391  euotd  5428  otiunsndisj  5435  tz7.2  5574  frsn  5675  dmopab2rex  5829  elsnxp  6198  reuop  6200  dfpo2  6203  ordtri1  6303  ordtri3  6306  fvmptdv2  6902  fveqressseq  6966  foco2  6992  fsn  7016  fnsnb  7047  fmptsng  7049  fmptsnd  7050  fconst2g  7087  fnprb  7093  fntpb  7094  funfvima  7115  soisoi  7208  isores3  7215  riotaeqimp  7268  eusvobj2  7277  ovmpodv2  7440  f1opw2  7533  sorpssun  7592  sorpssin  7593  oneqmin  7659  nlimsucg  7698  onzsl  7702  tfinds  7715  funcnvuni  7787  opiota  7908  mposn  7952  suppssov1  8023  suppssfv  8027  brtpos  8060  frrlem12  8122  frrlem13  8123  wfrlem10OLD  8158  wfrlem14OLD  8162  wfrlem15OLD  8163  seqomlem1  8290  seqomlem2  8291  omordi  8406  omord  8408  omwordi  8411  oeeui  8442  nnmordi  8471  nnmord  8472  nnmwordi  8475  nnawordex  8477  nnaordex  8478  nneob  8495  omsmolem  8496  eldifsucnn  8503  qsss  8576  eroveu  8610  mapsncnv  8690  ralxpmap  8693  elixpsn  8734  ixpsnf1o  8735  boxcutc  8738  pw2f1olem  8872  2pwne  8929  mapxpen  8939  mapunen  8942  php  9002  phpOLD  9014  onomeneq  9020  unxpdomlem2  9037  en1eqsnbi  9058  isfiniteg  9083  fofinf1o  9103  f1opwfi  9132  elfiun  9198  oieu  9307  brwdom2  9341  wdomtr  9343  ixpiunwdom  9358  en3lplem1  9379  suc11reg  9386  inf3lemd  9394  cantnfvalf  9432  cantnflt  9439  cantnfp1lem3  9447  cantnflem2  9457  ttrcltr  9483  rnttrcl  9489  ttrclselem1  9492  r1tr  9543  updjud  9701  dfac8alem  9794  wdomnumr  9829  isinfcard  9857  aceq3lem  9885  dfac5lem4  9891  dfac5  9893  dfac2b  9895  coftr  10038  fin23lem28  10105  fin23lem29  10106  fin1a2lem11  10175  fin1a2lem12  10176  fin1a2lem13  10177  hsmexlem9  10190  axdclem  10284  pwcfsdom  10348  gchdomtri  10394  fpwwe2  10408  gchpwdom  10435  gchhar  10444  addnidpi  10666  nqereu  10694  genpv  10764  genpdm  10767  distrlem5pr  10792  mulid1  10982  ltne  11081  mul02  11162  cnegex  11165  mul0or  11624  negfi  11933  sup2  11940  supaddc  11951  supadd  11952  supmul1  11953  supmul  11956  creur  11976  creui  11977  cju  11978  nnsub  12026  un0addcl  12275  un0mulcl  12276  nn0sub  12292  elz2  12346  zaddcl  12369  suprzcl2  12687  qmulz  12700  qre  12702  qnegcl  12715  elpqb  12725  xrmax1  12918  xrmin2  12921  max1ALT  12929  xlesubadd  13006  xmulass  13030  xlemul1a  13031  xrsupexmnf  13048  xrinfmexpnf  13049  xrub  13055  iccid  13133  fzsn  13307  fzsuc2  13323  fz1sbc  13341  elfzp12  13344  modmuladd  13642  seqid3  13776  bcval5  14041  bcpasc  14044  hashbnd  14059  hashnnn0genn0  14066  hashprg  14119  hashfzo  14153  wrdl1s1  14328  ccats1alpha  14333  cats1un  14443  shftlem  14788  replim  14836  absmod0  15024  absz  15032  rlimdm  15269  summolem2  15437  summo  15438  zsum  15439  fsum  15441  fsummulc2  15505  fsumconst  15511  fsum00  15519  incexclem  15557  isumsplit  15561  infcvgaux1i  15578  prodmolem2  15654  prodmo  15655  zprod  15656  fprod  15660  prodsn  15681  prodsnf  15683  fprodconst  15697  ruclem2  15950  fzo0dvdseq  16041  bitsf1ocnv  16160  sadcaddlem  16173  smueqlem  16206  gcdabs1  16245  bezoutlem1  16256  bezoutlem3  16258  bezoutlem4  16259  dvdsgcd  16261  dvdsmulgcd  16274  lcmgcdeq  16326  lcmf  16347  lcmfunsnlem1  16351  lcmfunsnlem2lem2  16353  isprm2lem  16395  dvdsprime  16401  isprm5  16421  coprm  16425  prmdvdsexpr  16431  rpexp  16436  phibndlem  16480  dfphi2  16484  hashgcdlem  16498  odzdvds  16505  nnoddn2prm  16521  pythagtriplem1  16526  iserodd  16545  pceulem  16555  pcqmul  16563  pcqcl  16566  pcxnn0cl  16570  pcxcl  16571  pcneg  16584  pcabs  16585  pcgcd1  16587  pcz  16591  pcprmpw2  16592  pcprmpw  16593  dvdsprmpweqle  16596  difsqpwdvds  16597  pcaddlem  16598  pcadd  16599  pcmpt  16602  pockthg  16616  prmreclem5  16630  4sqlem4  16662  mul4sq  16664  vdwapun  16684  vdwlem2  16692  vdwlem6  16696  vdwlem8  16698  vdwlem13  16703  0ram  16730  ram0  16732  ramcl  16739  cshwsiun  16810  wunress  16969  wunressOLD  16970  firest  17152  isssc  17541  pospo  18072  latnlej  18183  gsumval2a  18378  mnd1id  18436  0subm  18465  mulgnn0p1  18724  mulgnn0ass  18748  cyccom  18831  gicsubgen  18903  symg1bas  19007  snsymgefmndeq  19011  psgnunilem1  19110  psgnunilem2  19112  mndodcongi  19160  oddvdsnn0  19161  odnncl  19162  oddvds  19164  odeq  19167  odeq1  19176  pgpfi2  19220  sylow2a  19233  sylow2blem3  19236  sylow3lem6  19246  lsmelvalm  19265  lsmsubm  19267  lsmsubg  19268  lsmmod  19290  lsmdisj2  19297  efgmnvl  19329  efgtlen  19341  efgs1b  19351  efgrelexlemb  19365  efgredeu  19367  efgcpbllemb  19370  frgpuptinv  19386  frgpup3lem  19392  qusabl  19475  frgpnabllem1  19483  cyggeninv  19492  cyggenod  19493  cygablOLD  19501  gsumval3eu  19514  dprdssv  19628  dprdfeq0  19634  dprdsubg  19636  dprddisj2  19651  ablfacrp  19678  pgpfac1lem3  19689  pgpfaclem2  19694  dvreq1  19944  irredn1  19957  drngmul0or  20021  isabvd  20089  abvdom  20107  issrngd  20130  lmodfopnelem2  20169  lss1d  20234  lspsneq0  20283  lbspss  20353  lsmcl  20354  lvecvs0or  20379  lspindpi  20403  lidl1el  20498  lpiss  20530  lidldvgen  20535  nzrunit  20547  rrgeq0  20570  domneq0  20577  qsssubdrg  20666  zringlpirlem1  20693  znfld  20777  znunit  20780  znrrg  20782  cygznlem3  20786  frgpcyg  20790  psgnghm  20794  ipeq0  20852  cssincl  20902  lsmcss  20906  obselocv  20944  dsmmacl  20957  dsmmlss  20960  mplsubrglem  21219  mplmonmul  21246  mplcoe5lem  21249  mhpsclcl  21346  mhpvarcl  21347  coe1tmmul2  21456  coe1tmmul  21457  pf1ind  21530  mat1dimelbas  21629  mdetralt  21766  mdetunilem2  21771  mdetunilem7  21776  mdetunilem9  21778  maducoeval2  21798  chpscmat  22000  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  istopon  22070  eltg3  22121  tgidm  22139  clsval2  22210  opncldf1  22244  restbas  22318  tgrest  22319  restcld  22332  restcldr  22334  restcls  22341  restntr  22342  ordtbas2  22351  ordtbas  22352  ordtrest2lem  22363  ordtrest2  22364  pnfnei  22380  mnfnei  22381  tgcn  22412  cnconst  22444  cnindis  22452  lmss  22458  ordtt1  22539  discmp  22558  1stcrest  22613  2ndcdisj  22616  cldllycmp  22655  txbas  22727  ptpjpre1  22731  ptuni2  22736  ptbasin  22737  ptbasfi  22741  ptopn2  22744  txbasval  22766  ptpjopn  22772  ptclsg  22775  dfac14lem  22777  xkoccn  22779  ptcnp  22782  upxp  22783  ptrescn  22799  txkgen  22812  xkoptsub  22814  xkopt  22815  xkoco1cn  22817  xkoco2cn  22818  xkococn  22820  xkoinjcn  22847  ordthmeolem  22961  ptuncnv  22967  nrmhaus  22986  fbssint  22998  fbfinnfr  23001  fbasrn  23044  isufil2  23068  filufint  23080  rnelfm  23113  fmfnfmlem2  23115  fmfnfmlem3  23116  fmfnfmlem4  23117  fmfnfm  23118  flimtopon  23130  flimclslem  23144  fclstopon  23172  fclscf  23185  flimfnfcls  23188  alexsublem  23204  alexsubALTlem3  23209  alexsubALTlem4  23210  ptcmplem2  23213  tmdgsum2  23256  symgtgp  23266  cldsubg  23271  qustgplem  23281  tgptsmscld  23311  tsmsxplem1  23313  imasdsf1olem  23535  blssps  23586  blss  23587  stdbdxmet  23680  methaus  23685  metrest  23689  nrginvrcn  23865  nmoeq0  23909  blssioo  23967  xrtgioo  23978  xrsxmet  23981  reconnlem1  23998  reconnlem2  23999  xrge0tsms  24006  elcncf1di  24067  iccpnfcnv  24116  evth  24131  lebnumlem1  24133  lebnumlem2  24134  lebnumlem3  24135  nmoleub3  24291  minveclem3b  24601  ivthlem2  24625  ivthlem3  24626  elovolm  24648  ovolmge0  24650  ovoliun  24678  ovolicc2lem3  24692  ovolicc2  24695  voliunlem3  24725  dyaddisj  24769  dyadmax  24771  opnmblALT  24776  ismbfd  24812  ismbf2d  24813  mbfimaopnlem  24828  mbfimaopn2  24830  i1fmullem  24867  i1fres  24879  itg1climres  24888  mbfi1fseqlem4  24892  itg2lcl  24901  itgsplitioo  25011  ellimc2  25050  rolle  25163  dvlip  25166  dvge0  25179  dvne0  25184  lhop1lem  25186  tdeglem4  25233  tdeglem4OLD  25234  degltlem1  25246  deg1nn0clb  25264  deg1lt0  25265  dvdsq1p  25334  ply1rem  25337  fta1g  25341  elply2  25366  plyf  25368  ne0p  25377  plyeq0lem  25380  plypf1  25382  0dgrb  25416  coe1termlem  25428  dgrcolem2  25444  plymul0or  25450  plyrem  25474  fta1  25477  quotcan  25478  aalioulem3  25503  eff1olem  25713  lognegb  25754  eflogeq  25766  argregt0  25774  argrege0  25775  tanarg  25783  cxpexp  25832  cxpeq0  25842  mulcxp  25849  cxpeq  25919  atans2  26090  scvxcvx  26144  dmgmaddn0  26181  isppw2  26273  vmappw  26274  vmacl  26276  efvmacl  26278  isnsqf  26293  mumullem2  26338  sqff1o  26340  dvdsppwf1o  26344  ppiublem1  26359  vmalelog  26362  chtublem  26368  fsumvma  26370  perfectlem2  26387  perfect  26388  bposlem1  26441  lgsmod  26480  lgsne0  26492  lgsdirnn0  26501  lgsqr  26508  lgsdchr  26512  gausslemma2dlem1a  26522  gausslemma2dlem6  26529  lgseisenlem2  26533  lgsquadlem1  26537  lgsquadlem2  26538  2lgslem1b  26549  2sqlem2  26575  mul2sq  26576  2sqlem7  26581  dchrisum0fno1  26668  pntrsumbnd2  26724  ostthlem1  26784  ostth2lem2  26791  ostth3  26795  ostth  26796  colinearalg  27287  axpasch  27318  axlowdimlem16  27334  axlowdimlem17  27335  axlowdim  27338  axcontlem2  27342  axcontlem4  27344  axcontlem7  27347  lpvtx  27447  edglnl  27522  numedglnl  27523  usgredgop  27549  usgrexmplef  27635  uhgrspansubgrlem  27666  uhgrspan1  27679  nbusgredgeu0  27744  nb3grprlem2  27757  cusgrsize2inds  27829  vtxd0nedgb  27864  rusgrpropnb  27959  upgrwlkvtxedg  28021  wlkp1lem1  28050  wlkp1lem6  28055  wlkp1lem8  28057  usgr2wlkneq  28133  crctcshwlk  28196  crctcsh  28198  iswwlksnon  28227  wlkiswwlks1  28241  wwlksnextbi  28268  wwlksnextproplem2  28284  wspthsnonn0vne  28291  clwlkclwwlklem2  28373  clwwisshclwws  28388  erclwwlktr  28395  clwwlkel  28419  clwwlkext2edg  28429  erclwwlkntr  28444  clwlknf1oclwwlknlem2  28455  clwlknf1oclwwlknlem3  28456  clwlknf1oclwwlkn  28457  clwwlknonccat  28469  0wlkons1  28494  3wlkdlem6  28538  eupth2eucrct  28590  frgrwopreglem2  28686  2clwwlk2clwwlk  28723  wlkl0  28740  nvmul0or  29021  ipasslem5  29206  ipasslem11  29211  hvmul0or  29396  his6  29470  hhssnv  29635  ocsh  29654  ocin  29667  shsidmi  29755  chnlen0  29815  h1de2bi  29925  h1de2ctlem  29926  h1de2ci  29927  spansni  29928  3oalem1  30033  nmcexi  30397  atcveq0  30719  chcv1  30726  cdjreui  30803  cdj3lem2b  30808  xrge0tsmsd  31326  ccfldextdgrr  31751  ordtrest2NEWlem  31881  ordtrest2NEW  31882  xrge0iifcnv  31892  esumc  32028  esumpcvgval  32055  ballotlemfc0  32468  ballotlemfcc  32469  subfacp1lem4  33154  subfacp1lem5  33155  erdszelem8  33169  sconnpi1  33210  cvmsss2  33245  cvmlift2lem12  33285  satfv0  33329  satfv0fun  33342  satf00  33345  sat1el2xp  33350  fmla0xp  33354  fmlasucdisj  33370  satffunlem1lem1  33373  satffunlem2lem1  33375  dmopab3rexdif  33376  msubco  33502  msubvrs  33531  sinccvglem  33639  untsucf  33660  nnuni  33701  eqfunresadj  33744  dfrdg2  33780  frpoins3xpg  33796  frpoins3xp3g  33797  poxp2  33799  xpord2pred  33801  sexp2  33802  poxp3  33805  xpord3pred  33807  nolesgn2ores  33884  nogesgn1ores  33886  nolt02o  33907  nogt01o  33908  nosupbnd2  33928  noinfbnd2lem1  33942  noetasuplem4  33948  noetainflem4  33952  madef  34049  sltlpss  34096  lrrecfr  34109  addsval  34135  colineardim1  34372  btwnconn1lem14  34411  segleantisym  34426  colinbtwnle  34429  outsidele  34443  lineunray  34458  linethru  34464  elicc3  34515  opnregcld  34528  cldregopn  34529  fnejoin2  34567  bj-isrvec  35474  dissneqlem  35520  icorempo  35531  relowlssretop  35543  relowlpssretop  35544  rdgssun  35558  finxpsuclem  35577  lindsenlbs  35781  ptrecube  35786  poimirlem6  35792  poimirlem7  35793  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  itg2addnclem3  35839  ftc1anclem6  35864  dvasin  35870  unirep  35880  sdclem2  35909  ssbnd  35955  prdsbnd  35960  cntotbnd  35963  heibor1lem  35976  rrnequiv  36002  ismndo2  36041  grpoeqdivid  36048  isdrngo3  36126  crngohomfo  36173  0idl  36192  1idl  36193  divrngidl  36195  smprngopr  36219  prnc  36234  ispridlc  36237  riotaclbgBAD  36975  lshpdisj  37008  lsateln0  37016  lsatcveq0  37053  opnlen0  37209  cmtbr4N  37276  cvrnbtwn2  37296  cvrnbtwn4  37300  atcvreq0  37335  cvlatexch1  37357  exatleN  37425  atlelt  37459  ps-2  37499  llnn0  37537  lplnn0N  37568  islpln2a  37569  lvoln0N  37612  islvol2aN  37613  4at  37634  dalemcea  37681  dalem3  37685  pmapglb2N  37792  pmapglb2xN  37793  cdlema1N  37812  cdlemb  37815  paddasslem17  37857  llnexchb2lem  37889  llnexchb2  37890  lhpat3  38067  ltrnid  38156  trlne  38206  cdlemc4  38215  cdleme11h  38287  cdlemednuN  38321  cdlemg1a  38591  tendoeq2  38795  tendoid0  38846  dva1dim  39006  dib1dim  39186  dihlatat  39358  dochkrshp4  39410  dochkr1  39499  lclkrlem2e  39532  lcfrlem16  39579  lcfrlem28  39591  mapd0  39686  hdmap14lem13  39901  fnsnbt  40215  frlmsnic  40270  dvdsexpnn0  40348  reladdrsub  40375  sn-negex12  40405  sn-mulid2  40424  sn-mul02  40429  mulgt0con1d  40435  mulgt0con2d  40436  sn-sup2  40446  prjspner1  40470  prjcrv0  40477  elrfi  40523  mrefg2  40536  eldiophb  40586  eldioph2b  40592  diophin  40601  diophun  40602  rexzrexnn0  40633  eldioph4b  40640  diophren  40642  rencldnfilem  40649  pellexlem6  40663  jm2.19  40822  rmydioph  40843  expdiophlem1  40850  expdioph  40852  lnr2i  40948  lpirlnr  40949  hbtlem2  40956  hbtlem4  40958  hbtlem6  40961  dgrsub2  40967  dgraa0p  40981  rngunsnply  41005  nlimsuc  41055  dfsucon  41137  radcnvrat  41939  pm14.24  42057  addrcom  42100  afveu  44656  dfafn5b  44664  rlimdmafv  44680  afv2eu  44741  rlimdmafv2  44761  el1fzopredsuc  44828  elsetpreimafvssdm  44849  imasetpreimafvbijlemfo  44868  sprvalpw  44943  prprvalpw  44978  reupr  44985  fmtnofac2lem  45031  proththdlem  45076  perfectALTVlem2  45185  perfectALTV  45186  gbowpos  45222  gbowgt5  45225  gboge9  45227  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  isomuspgr  45297  lincellss  45778  lindsrng01  45820  suppdm  45862  nnpw2pb  45944  0aryfvalel  45991  0aryfvalelfv  45992  itsclc0xyqsolr  46126  natlocalincr  46522