Theorem syl5ibrcom 236

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  biimprcd  239  elsn2g  4157  preq1b  4317  elpreqprb  4335  reusv2lem2OLD  4796  reusv3  4802  alxfr  4804  reuhypd  4821  opth1  4870  euotd  4900  otiunsndisj  4905  tz7.2  5022  frsn  5112  elsnxp  5594  ordtri1  5673  ordtri3  5676  fvmptdv2  6206  fveqressseq  6263  foco2  6287  foco2OLD  6288  fsn  6308  fnsnb  6337  fmptsng  6339  fmptsnd  6340  fconst2g  6373  fnprb  6377  fntpb  6378  funfvima  6396  soisoi  6478  isores3  6485  eusvobj2  6542  ovmpt2dv2  6692  f1opw2  6786  sorpssun  6842  sorpssin  6843  oneqmin  6897  nlimsucg  6934  onzsl  6938  tfinds  6951  funcnvuni  7012  opiota  7118  mpt2sn  7155  suppssov1  7214  suppssfv  7218  brtpos  7248  wfrlem10  7311  wfrlem14  7315  wfrlem15  7316  seqomlem1  7432  seqomlem2  7433  omordi  7533  omord  7535  omwordi  7538  oeeui  7569  nnmordi  7598  nnmord  7599  nnmwordi  7602  nnawordex  7604  nnaordex  7605  nneob  7619  omsmolem  7620  qsss  7695  eroveu  7729  mapsncnv  7790  ralxpmap  7793  elixpsn  7833  ixpsnf1o  7834  boxcutc  7837  pw2f1olem  7949  2pwne  8001  mapxpen  8011  mapunen  8014  php  8029  unxpdomlem2  8050  en1eqsnbi  8076  isfiniteg  8105  fofinf1o  8126  f1opwfi  8153  elfiun  8219  oieu  8327  brwdom2  8361  wdomtr  8363  ixpiunwdom  8379  en3lplem1  8394  suc11reg  8399  inf3lemd  8407  cantnfvalf  8445  cantnflt  8452  cantnfp1lem3  8460  cantnflem2  8470  r1tr  8522  dfac8alem  8735  wdomnumr  8770  isinfcard  8798  aceq3lem  8826  dfac5lem4  8832  dfac5  8834  dfac2  8836  coftr  8978  fin23lem28  9045  fin23lem29  9046  fin1a2lem11  9115  fin1a2lem12  9116  fin1a2lem13  9117  hsmexlem9  9130  axdclem  9224  pwcfsdom  9284  gchdomtri  9330  fpwwe2  9344  gchpwdom  9371  gchhar  9380  addnidpi  9602  nqereu  9630  genpv  9700  genpdm  9703  distrlem5pr  9728  mulid1  9916  ltne  10013  mul02  10093  cnegex  10096  mul0or  10546  negfi  10850  sup2  10858  supaddc  10867  supadd  10868  supmul1  10869  supmul  10872  creur  10891  creui  10892  cju  10893  nnsub  10936  un0addcl  11203  un0mulcl  11204  nn0sub  11220  elz2  11271  zaddcl  11294  suprzcl2  11654  qmulz  11667  qre  11669  qnegcl  11681  xrmax1  11880  xrmin2  11883  max1ALT  11891  xlesubadd  11965  xmulass  11989  xlemul1a  11990  xrsupexmnf  12007  xrinfmexpnf  12008  xrub  12014  iccid  12091  fzsn  12254  fzsuc2  12268  fz1sbc  12285  elfzp12  12288  modmuladd  12574  seqid3  12707  bcval5  12967  bcpasc  12970  hashbnd  12985  hashnnn0genn0  12993  hashprg  13043  hashprgOLD  13044  hashfzo  13076  wrdl1s1  13247  cats1un  13327  shftlem  13656  replim  13704  absmod0  13891  absz  13899  rlimdm  14130  summolem2  14294  summo  14295  zsum  14296  fsum  14298  fsummulc2  14358  fsumconst  14364  fsum00  14371  incexclem  14407  isumsplit  14411  infcvgaux1i  14428  prodmolem2  14504  prodmo  14505  zprod  14506  fprod  14510  prodsn  14531  prodsnf  14533  fprodconst  14547  ruclem2  14800  fzo0dvdseq  14883  bitsf1ocnv  15004  sadcaddlem  15017  smueqlem  15050  gcdabs1  15089  bezoutlem1  15094  bezoutlem3  15096  bezoutlem4  15097  dvdsgcd  15099  dvdsmulgcd  15112  lcmgcdeq  15163  lcmf  15184  lcmfunsnlem1  15188  lcmfunsnlem2lem2  15190  dvdsprime  15238  isprm5  15257  coprm  15261  prmdvdsexpr  15267  rpexp  15270  phibndlem  15313  dfphi2  15317  hashgcdlem  15331  odzdvds  15338  nnoddn2prm  15354  pythagtriplem1  15359  iserodd  15378  pceulem  15388  pcqmul  15396  pcqcl  15399  pcxcl  15403  pcneg  15416  pcabs  15417  pcgcd1  15419  pcz  15423  pcprmpw2  15424  pcprmpw  15425  dvdsprmpweqle  15428  difsqpwdvds  15429  pcaddlem  15430  pcadd  15431  pcmpt  15434  pockthg  15448  prmreclem5  15462  4sqlem4  15494  mul4sq  15496  vdwapun  15516  vdwlem2  15524  vdwlem6  15528  vdwlem8  15530  vdwlem13  15535  0ram  15562  ram0  15564  ramcl  15571  cshwsiun  15644  wunress  15767  firest  15916  xpscfv  16045  isssc  16303  pospo  16796  latnlej  16891  gsumval2a  17102  mnd1id  17155  mulgnn0p1  17375  mulgnn0ass  17401  gicsubgen  17544  symg1bas  17639  psgnunilem1  17736  psgnunilem2  17738  mndodcongi  17785  oddvdsnn0  17786  odnncl  17787  oddvds  17789  odeq  17792  odeq1  17800  pgpfi2  17844  sylow2a  17857  sylow2blem3  17860  sylow3lem6  17870  lsmelvalm  17889  lsmsubm  17891  lsmsubg  17892  lsmmod  17911  lsmdisj2  17918  efgmnvl  17950  efgtlen  17962  efgs1b  17972  efgrelexlemb  17986  efgredeu  17988  efgcpbllemb  17991  frgpuptinv  18007  frgpup3lem  18013  qusabl  18091  frgpnabllem1  18099  cyggeninv  18108  cyggenod  18109  cygabl  18115  gsumval3eu  18128  dprdssv  18238  dprdfeq0  18244  dprdsubg  18246  dprddisj2  18261  ablfacrp  18288  pgpfac1lem3  18299  pgpfaclem2  18304  dvreq1  18516  irredn1  18529  drngmul0or  18591  isabvd  18643  abvdom  18661  issrngd  18684  lmodfopnelem2  18723  lss1d  18784  lspsneq0  18833  lbspss  18903  lsmcl  18904  lvecvs0or  18929  lspindpi  18953  lidl1el  19039  lpiss  19071  lidldvgen  19076  nzrunit  19088  rrgeq0  19111  domneq0  19118  mplsubrglem  19260  mplmonmul  19285  mplcoe5lem  19288  coe1tmmul2  19467  coe1tmmul  19468  pf1ind  19540  qsssubdrg  19624  zringlpirlem1  19651  znfld  19728  znunit  19731  znrrg  19733  cygznlem3  19737  frgpcyg  19741  psgnghm  19745  ipeq0  19802  cssincl  19851  lsmcss  19855  obselocv  19891  dsmmacl  19904  dsmmlss  19907  mat1dimelbas  20096  mdetralt  20233  mdetunilem2  20238  mdetunilem7  20243  mdetunilem9  20245  maducoeval2  20265  chpscmat  20466  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  istopon  20540  eltg3  20577  tgidm  20595  clsval2  20664  opncldf1  20698  restbas  20772  tgrest  20773  restcld  20786  restcldr  20788  restcls  20795  restntr  20796  ordtbas2  20805  ordtbas  20806  ordtrest2lem  20817  ordtrest2  20818  pnfnei  20834  mnfnei  20835  tgcn  20866  cnconst  20898  cnindis  20906  lmss  20912  ordtt1  20993  discmp  21011  1stcrest  21066  2ndcdisj  21069  cldllycmp  21108  txbas  21180  ptpjpre1  21184  ptuni2  21189  ptbasin  21190  ptbasfi  21194  ptopn2  21197  txbasval  21219  ptpjopn  21225  ptclsg  21228  dfac14lem  21230  xkoccn  21232  ptcnp  21235  upxp  21236  ptrescn  21252  txkgen  21265  xkoptsub  21267  xkopt  21268  xkoco1cn  21270  xkoco2cn  21271  xkococn  21273  xkoinjcn  21300  ordthmeolem  21414  ptuncnv  21420  nrmhaus  21439  fbssint  21452  fbfinnfr  21455  fbasrn  21498  isufil2  21522  filufint  21534  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem3  21570  fmfnfmlem4  21571  fmfnfm  21572  flimtopon  21584  flimclslem  21598  fclstopon  21626  fclscf  21639  flimfnfcls  21642  alexsublem  21658  alexsubALTlem3  21663  alexsubALTlem4  21664  ptcmplem2  21667  tmdgsum2  21710  symgtgp  21715  cldsubg  21724  qustgplem  21734  tgptsmscld  21764  tsmsxplem1  21766  imasdsf1olem  21988  blssps  22039  blss  22040  stdbdxmet  22130  methaus  22135  metrest  22139  nrginvrcn  22306  nmoeq0  22350  blssioo  22406  xrtgioo  22417  xrsxmet  22420  reconnlem1  22437  reconnlem2  22438  xrge0tsms  22445  elcncf1di  22506  iccpnfcnv  22551  evth  22566  lebnumlem1  22568  lebnumlem2  22569  lebnumlem3  22570  nmoleub3  22727  minveclem3b  23007  ivthlem2  23028  ivthlem3  23029  elovolm  23050  ovolmge0  23052  ovoliun  23080  ovolicc2lem3  23094  ovolicc2  23097  voliunlem3  23127  dyaddisj  23170  dyadmax  23172  opnmblALT  23177  ismbfd  23213  ismbf2d  23214  mbfimaopnlem  23228  mbfimaopn2  23230  i1fmullem  23267  i1fres  23278  itg1climres  23287  mbfi1fseqlem4  23291  itg2lcl  23300  itgsplitioo  23410  ellimc2  23447  rolle  23557  dvlip  23560  dvge0  23573  dvne0  23578  lhop1lem  23580  tdeglem4  23624  degltlem1  23636  deg1nn0clb  23654  deg1lt0  23655  dvdsq1p  23724  ply1rem  23727  fta1g  23731  elply2  23756  plyf  23758  ne0p  23767  plyeq0lem  23770  plypf1  23772  0dgrb  23806  coe1termlem  23818  dgrcolem2  23834  plymul0or  23840  plyrem  23864  fta1  23867  quotcan  23868  aalioulem3  23893  eff1olem  24098  lognegb  24140  eflogeq  24152  argregt0  24160  argrege0  24161  tanarg  24169  cxpexp  24214  cxpeq0  24224  mulcxp  24231  cxpeq  24298  atans2  24458  scvxcvx  24512  dmgmaddn0  24549  isppw2  24641  vmappw  24642  vmacl  24644  efvmacl  24646  isnsqf  24661  mumullem2  24706  sqff1o  24708  dvdsppwf1o  24712  ppiublem1  24727  vmalelog  24730  chtublem  24736  fsumvma  24738  perfectlem2  24755  perfect  24756  bposlem1  24809  lgsmod  24848  lgsne0  24860  lgsdirnn0  24869  lgsqr  24876  lgsdchr  24880  gausslemma2dlem1a  24890  gausslemma2dlem6  24897  lgseisenlem2  24901  lgsquadlem1  24905  lgsquadlem2  24906  2lgslem1b  24917  2sqlem2  24943  mul2sq  24944  2sqlem7  24949  dchrisum0fno1  25000  pntrsumbnd2  25056  ostthlem1  25116  ostth2lem2  25123  ostth3  25127  ostth  25128  colinearalg  25590  axpasch  25621  axlowdimlem16  25637  axlowdimlem17  25638  axlowdim  25641  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  lpvtx  25734  usgraexmplef  25929  nbgraf1olem1  25970  nbgraf1olem3  25972  nbgraf1olem5  25974  nb3graprlem2  25981  cusgrasize2inds  26005  wlklenvm1  26060  wlkiswwlksur  26247  wwlknextbi  26253  wwlkextproplem2  26270  clwlkisclwwlklem1  26315  clwwisshclww  26335  erclwwlktr  26343  erclwwlkntr  26355  clwlkfclwwlk1hash  26369  vdgr1a  26433  vdusgra0nedg  26435  usgravd0nedg  26445  0eusgraiff0rgra  26466  rusgraprop2  26469  eupap1  26503  vdn0frgrav2  26550  vdgn0frgrav2  26551  nvmul0or  26889  ipasslem5  27074  ipasslem11  27079  hvmul0or  27266  his6  27340  hhssnv  27505  ocsh  27526  ocin  27539  shsidmi  27627  chnlen0  27687  h1de2bi  27797  h1de2ctlem  27798  h1de2ci  27799  spansni  27800  3oalem1  27905  nmcexi  28269  atcveq0  28591  chcv1  28598  cdjreui  28675  cdj3lem2b  28680  xrge0tsmsd  29116  ordtrest2NEWlem  29296  ordtrest2NEW  29297  xrge0iifcnv  29307  esumc  29440  esumpcvgval  29467  ballotlemfc0  29881  ballotlemfcc  29882  bnj145OLD  30049  subfacp1lem4  30419  subfacp1lem5  30420  erdszelem8  30434  sconpi1  30475  cvmsss2  30510  cvmlift2lem12  30550  msubco  30682  msubvrs  30711  sinccvglem  30820  untsucf  30841  dfpo2  30898  dfrdg2  30945  trpred0  30980  frrlem4  31027  colineardim1  31338  btwnconn1lem14  31377  segleantisym  31392  colinbtwnle  31395  outsidele  31409  lineunray  31424  linethru  31430  elicc3  31481  opnregcld  31495  cldregopn  31496  fnejoin2  31534  dissneqlem  32363  icorempt2  32375  relowlssretop  32387  relowlpssretop  32388  finxpsuclem  32410  lindsenlbs  32574  ptrecube  32579  poimirlem6  32585  poimirlem7  32586  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  itg2addnclem3  32633  ftc1anclem6  32660  dvasin  32666  unirep  32677  sdclem2  32708  ssbnd  32757  prdsbnd  32762  cntotbnd  32765  heibor1lem  32778  rrnequiv  32804  ismndo2  32843  grpoeqdivid  32850  isdrngo3  32928  crngohomfo  32975  0idl  32994  1idl  32995  divrngidl  32997  smprngopr  33021  prnc  33036  ispridlc  33039  riotaclbgBAD  33258  lshpdisj  33292  lsateln0  33300  lsatcveq0  33337  opnlen0  33493  cmtbr4N  33560  cvrnbtwn2  33580  cvrnbtwn4  33584  atcvreq0  33619  cvlatexch1  33641  exatleN  33708  atlelt  33742  ps-2  33782  llnn0  33820  lplnn0N  33851  islpln2a  33852  lvoln0N  33895  islvol2aN  33896  4at  33917  dalemcea  33964  dalem3  33968  pmapglb2N  34075  pmapglb2xN  34076  cdlema1N  34095  cdlemb  34098  paddasslem17  34140  llnexchb2lem  34172  llnexchb2  34173  lhpat3  34350  ltrnid  34439  trlne  34490  cdlemc4  34499  cdleme11h  34571  cdlemednuN  34605  cdlemg1a  34876  tendoeq2  35080  tendoid0  35131  dva1dim  35291  dib1dim  35472  dihlatat  35644  dochkrshp4  35696  dochkr1  35785  lclkrlem2e  35818  lcfrlem16  35865  lcfrlem28  35877  mapd0  35972  hdmap14lem13  36190  elrfi  36275  mrefg2  36288  eldiophb  36338  eldioph2b  36344  diophin  36354  diophun  36355  rexzrexnn0  36386  eldioph4b  36393  diophren  36395  rencldnfilem  36402  pellexlem6  36416  jm2.19  36578  rmydioph  36599  expdiophlem1  36606  expdioph  36608  lnr2i  36705  lpirlnr  36706  hbtlem2  36713  hbtlem4  36715  hbtlem6  36718  dgrsub2  36724  dgraa0p  36738  rngunsnply  36762  radcnvrat  37535  pm14.24  37655  addrcom  37700  afveu  39882  dfafn5b  39890  rlimdmafv  39906  el1fzopredsuc  39948  fmtnofac2lem  40018  proththdlem  40068  perfectALTVlem2  40165  perfectALTV  40166  gbopos  40181  gbogt5  40184  gboage9  40186  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  riotaeqimp  40338  uhgrauhgr  40376  usgredgop  40400  uhgrspansubgrlem  40514  uhgrspan1  40527  nbusgredgeu0  40596  nb3grprlem2  40609  cusgrsize2inds  40669  vtxd0nedgb  40703  rusgrpropnb  40783  upgr1wlkvtxedg  40853  1wlkp1lem1  40882  1wlkp1lem6  40887  1wlkp1lem8  40889  usgr2wlkneq  40962  crctcsh1wlk  41025  crctcsh  41027  1wlkiswwlks1  41064  wlkwwlksur  41094  wwlksnextbi  41100  wwlksnextproplem2  41116  wspthsnonn0vne  41124  clwlkclwwlklem2  41209  clwwlksext2edg  41230  clwwisshclwws  41235  erclwwlkstr  41243  erclwwlksntr  41255  clwlksfclwwlk1hash  41267  0wlkOns1  41289  31wlkdlem6  41332  eupth2eucrct  41385  lincellss  42009  lindsrng01  42051  suppdm  42094  nnpw2pb  42179