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  4596  preq1b  4774  elpreqprb  4795  reusv3  5323  alxfr  5325  reuhypd  5337  opth1  5384  euotd  5421  otiunsndisj  5428  tz7.2  5564  frsn  5665  dmopab2rex  5815  elsnxp  6183  reuop  6185  dfpo2  6188  ordtri1  6284  ordtri3  6287  fvmptdv2  6875  fveqressseq  6939  foco2  6965  fsn  6989  fnsnb  7020  fmptsng  7022  fmptsnd  7023  fconst2g  7060  fnprb  7066  fntpb  7067  funfvima  7088  soisoi  7179  isores3  7186  riotaeqimp  7239  eusvobj2  7248  ovmpodv2  7409  f1opw2  7502  sorpssun  7561  sorpssin  7562  oneqmin  7627  nlimsucg  7664  onzsl  7668  tfinds  7681  funcnvuni  7752  opiota  7872  mposn  7914  suppssov1  7985  suppssfv  7989  brtpos  8022  frrlem12  8084  frrlem13  8085  wfrlem10OLD  8120  wfrlem14OLD  8124  wfrlem15OLD  8125  seqomlem1  8251  seqomlem2  8252  omordi  8359  omord  8361  omwordi  8364  oeeui  8395  nnmordi  8424  nnmord  8425  nnmwordi  8428  nnawordex  8430  nnaordex  8431  nneob  8446  omsmolem  8447  qsss  8525  eroveu  8559  mapsncnv  8639  ralxpmap  8642  elixpsn  8683  ixpsnf1o  8684  boxcutc  8687  pw2f1olem  8816  2pwne  8869  mapxpen  8879  mapunen  8882  php  8897  unxpdomlem2  8957  en1eqsnbi  8978  isfiniteg  9004  fofinf1o  9024  f1opwfi  9053  elfiun  9119  oieu  9228  brwdom2  9262  wdomtr  9264  ixpiunwdom  9279  en3lplem1  9300  suc11reg  9307  inf3lemd  9315  cantnfvalf  9353  cantnflt  9360  cantnfp1lem3  9368  cantnflem2  9378  trpred0  9410  r1tr  9465  updjud  9623  dfac8alem  9716  wdomnumr  9751  isinfcard  9779  aceq3lem  9807  dfac5lem4  9813  dfac5  9815  dfac2b  9817  coftr  9960  fin23lem28  10027  fin23lem29  10028  fin1a2lem11  10097  fin1a2lem12  10098  fin1a2lem13  10099  hsmexlem9  10112  axdclem  10206  pwcfsdom  10270  gchdomtri  10316  fpwwe2  10330  gchpwdom  10357  gchhar  10366  addnidpi  10588  nqereu  10616  genpv  10686  genpdm  10689  distrlem5pr  10714  mulid1  10904  ltne  11002  mul02  11083  cnegex  11086  mul0or  11545  negfi  11854  sup2  11861  supaddc  11872  supadd  11873  supmul1  11874  supmul  11877  creur  11897  creui  11898  cju  11899  nnsub  11947  un0addcl  12196  un0mulcl  12197  nn0sub  12213  elz2  12267  zaddcl  12290  suprzcl2  12607  qmulz  12620  qre  12622  qnegcl  12635  elpqb  12645  xrmax1  12838  xrmin2  12841  max1ALT  12849  xlesubadd  12926  xmulass  12950  xlemul1a  12951  xrsupexmnf  12968  xrinfmexpnf  12969  xrub  12975  iccid  13053  fzsn  13227  fzsuc2  13243  fz1sbc  13261  elfzp12  13264  modmuladd  13561  seqid3  13695  bcval5  13960  bcpasc  13963  hashbnd  13978  hashnnn0genn0  13985  hashprg  14038  hashfzo  14072  wrdl1s1  14247  ccats1alpha  14252  cats1un  14362  shftlem  14707  replim  14755  absmod0  14943  absz  14951  rlimdm  15188  summolem2  15356  summo  15357  zsum  15358  fsum  15360  fsummulc2  15424  fsumconst  15430  fsum00  15438  incexclem  15476  isumsplit  15480  infcvgaux1i  15497  prodmolem2  15573  prodmo  15574  zprod  15575  fprod  15579  prodsn  15600  prodsnf  15602  fprodconst  15616  ruclem2  15869  fzo0dvdseq  15960  bitsf1ocnv  16079  sadcaddlem  16092  smueqlem  16125  gcdabs1  16164  bezoutlem1  16175  bezoutlem3  16177  bezoutlem4  16178  dvdsgcd  16180  dvdsmulgcd  16193  lcmgcdeq  16245  lcmf  16266  lcmfunsnlem1  16270  lcmfunsnlem2lem2  16272  isprm2lem  16314  dvdsprime  16320  isprm5  16340  coprm  16344  prmdvdsexpr  16350  rpexp  16355  phibndlem  16399  dfphi2  16403  hashgcdlem  16417  odzdvds  16424  nnoddn2prm  16440  pythagtriplem1  16445  iserodd  16464  pceulem  16474  pcqmul  16482  pcqcl  16485  pcxnn0cl  16489  pcxcl  16490  pcneg  16503  pcabs  16504  pcgcd1  16506  pcz  16510  pcprmpw2  16511  pcprmpw  16512  dvdsprmpweqle  16515  difsqpwdvds  16516  pcaddlem  16517  pcadd  16518  pcmpt  16521  pockthg  16535  prmreclem5  16549  4sqlem4  16581  mul4sq  16583  vdwapun  16603  vdwlem2  16611  vdwlem6  16615  vdwlem8  16617  vdwlem13  16622  0ram  16649  ram0  16651  ramcl  16658  cshwsiun  16729  wunress  16886  wunressOLD  16887  firest  17060  isssc  17449  pospo  17978  latnlej  18089  gsumval2a  18284  mnd1id  18342  0subm  18371  mulgnn0p1  18630  mulgnn0ass  18654  cyccom  18737  gicsubgen  18809  symg1bas  18913  snsymgefmndeq  18917  psgnunilem1  19016  psgnunilem2  19018  mndodcongi  19066  oddvdsnn0  19067  odnncl  19068  oddvds  19070  odeq  19073  odeq1  19082  pgpfi2  19126  sylow2a  19139  sylow2blem3  19142  sylow3lem6  19152  lsmelvalm  19171  lsmsubm  19173  lsmsubg  19174  lsmmod  19196  lsmdisj2  19203  efgmnvl  19235  efgtlen  19247  efgs1b  19257  efgrelexlemb  19271  efgredeu  19273  efgcpbllemb  19276  frgpuptinv  19292  frgpup3lem  19298  qusabl  19381  frgpnabllem1  19389  cyggeninv  19398  cyggenod  19399  cygablOLD  19407  gsumval3eu  19420  dprdssv  19534  dprdfeq0  19540  dprdsubg  19542  dprddisj2  19557  ablfacrp  19584  pgpfac1lem3  19595  pgpfaclem2  19600  dvreq1  19850  irredn1  19863  drngmul0or  19927  isabvd  19995  abvdom  20013  issrngd  20036  lmodfopnelem2  20075  lss1d  20140  lspsneq0  20189  lbspss  20259  lsmcl  20260  lvecvs0or  20285  lspindpi  20309  lidl1el  20402  lpiss  20434  lidldvgen  20439  nzrunit  20451  rrgeq0  20474  domneq0  20481  qsssubdrg  20569  zringlpirlem1  20596  znfld  20680  znunit  20683  znrrg  20685  cygznlem3  20689  frgpcyg  20693  psgnghm  20697  ipeq0  20755  cssincl  20805  lsmcss  20809  obselocv  20845  dsmmacl  20858  dsmmlss  20861  mplsubrglem  21120  mplmonmul  21147  mplcoe5lem  21150  mhpsclcl  21247  mhpvarcl  21248  coe1tmmul2  21357  coe1tmmul  21358  pf1ind  21431  mat1dimelbas  21528  mdetralt  21665  mdetunilem2  21670  mdetunilem7  21675  mdetunilem9  21677  maducoeval2  21697  chpscmat  21899  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  istopon  21969  eltg3  22020  tgidm  22038  clsval2  22109  opncldf1  22143  restbas  22217  tgrest  22218  restcld  22231  restcldr  22233  restcls  22240  restntr  22241  ordtbas2  22250  ordtbas  22251  ordtrest2lem  22262  ordtrest2  22263  pnfnei  22279  mnfnei  22280  tgcn  22311  cnconst  22343  cnindis  22351  lmss  22357  ordtt1  22438  discmp  22457  1stcrest  22512  2ndcdisj  22515  cldllycmp  22554  txbas  22626  ptpjpre1  22630  ptuni2  22635  ptbasin  22636  ptbasfi  22640  ptopn2  22643  txbasval  22665  ptpjopn  22671  ptclsg  22674  dfac14lem  22676  xkoccn  22678  ptcnp  22681  upxp  22682  ptrescn  22698  txkgen  22711  xkoptsub  22713  xkopt  22714  xkoco1cn  22716  xkoco2cn  22717  xkococn  22719  xkoinjcn  22746  ordthmeolem  22860  ptuncnv  22866  nrmhaus  22885  fbssint  22897  fbfinnfr  22900  fbasrn  22943  isufil2  22967  filufint  22979  rnelfm  23012  fmfnfmlem2  23014  fmfnfmlem3  23015  fmfnfmlem4  23016  fmfnfm  23017  flimtopon  23029  flimclslem  23043  fclstopon  23071  fclscf  23084  flimfnfcls  23087  alexsublem  23103  alexsubALTlem3  23108  alexsubALTlem4  23109  ptcmplem2  23112  tmdgsum2  23155  symgtgp  23165  cldsubg  23170  qustgplem  23180  tgptsmscld  23210  tsmsxplem1  23212  imasdsf1olem  23434  blssps  23485  blss  23486  stdbdxmet  23577  methaus  23582  metrest  23586  nrginvrcn  23762  nmoeq0  23806  blssioo  23864  xrtgioo  23875  xrsxmet  23878  reconnlem1  23895  reconnlem2  23896  xrge0tsms  23903  elcncf1di  23964  iccpnfcnv  24013  evth  24028  lebnumlem1  24030  lebnumlem2  24031  lebnumlem3  24032  nmoleub3  24188  minveclem3b  24497  ivthlem2  24521  ivthlem3  24522  elovolm  24544  ovolmge0  24546  ovoliun  24574  ovolicc2lem3  24588  ovolicc2  24591  voliunlem3  24621  dyaddisj  24665  dyadmax  24667  opnmblALT  24672  ismbfd  24708  ismbf2d  24709  mbfimaopnlem  24724  mbfimaopn2  24726  i1fmullem  24763  i1fres  24775  itg1climres  24784  mbfi1fseqlem4  24788  itg2lcl  24797  itgsplitioo  24907  ellimc2  24946  rolle  25059  dvlip  25062  dvge0  25075  dvne0  25080  lhop1lem  25082  tdeglem4  25129  tdeglem4OLD  25130  degltlem1  25142  deg1nn0clb  25160  deg1lt0  25161  dvdsq1p  25230  ply1rem  25233  fta1g  25237  elply2  25262  plyf  25264  ne0p  25273  plyeq0lem  25276  plypf1  25278  0dgrb  25312  coe1termlem  25324  dgrcolem2  25340  plymul0or  25346  plyrem  25370  fta1  25373  quotcan  25374  aalioulem3  25399  eff1olem  25609  lognegb  25650  eflogeq  25662  argregt0  25670  argrege0  25671  tanarg  25679  cxpexp  25728  cxpeq0  25738  mulcxp  25745  cxpeq  25815  atans2  25986  scvxcvx  26040  dmgmaddn0  26077  isppw2  26169  vmappw  26170  vmacl  26172  efvmacl  26174  isnsqf  26189  mumullem2  26234  sqff1o  26236  dvdsppwf1o  26240  ppiublem1  26255  vmalelog  26258  chtublem  26264  fsumvma  26266  perfectlem2  26283  perfect  26284  bposlem1  26337  lgsmod  26376  lgsne0  26388  lgsdirnn0  26397  lgsqr  26404  lgsdchr  26408  gausslemma2dlem1a  26418  gausslemma2dlem6  26425  lgseisenlem2  26429  lgsquadlem1  26433  lgsquadlem2  26434  2lgslem1b  26445  2sqlem2  26471  mul2sq  26472  2sqlem7  26477  dchrisum0fno1  26564  pntrsumbnd2  26620  ostthlem1  26680  ostth2lem2  26687  ostth3  26691  ostth  26692  colinearalg  27181  axpasch  27212  axlowdimlem16  27228  axlowdimlem17  27229  axlowdim  27232  axcontlem2  27236  axcontlem4  27238  axcontlem7  27241  lpvtx  27341  edglnl  27416  numedglnl  27417  usgredgop  27443  usgrexmplef  27529  uhgrspansubgrlem  27560  uhgrspan1  27573  nbusgredgeu0  27638  nb3grprlem2  27651  cusgrsize2inds  27723  vtxd0nedgb  27758  rusgrpropnb  27853  upgrwlkvtxedg  27914  wlkp1lem1  27943  wlkp1lem6  27948  wlkp1lem8  27950  usgr2wlkneq  28025  crctcshwlk  28088  crctcsh  28090  iswwlksnon  28119  wlkiswwlks1  28133  wwlksnextbi  28160  wwlksnextproplem2  28176  wspthsnonn0vne  28183  clwlkclwwlklem2  28265  clwwisshclwws  28280  erclwwlktr  28287  clwwlkel  28311  clwwlkext2edg  28321  erclwwlkntr  28336  clwlknf1oclwwlknlem2  28347  clwlknf1oclwwlknlem3  28348  clwlknf1oclwwlkn  28349  clwwlknonccat  28361  0wlkons1  28386  3wlkdlem6  28430  eupth2eucrct  28482  frgrwopreglem2  28578  2clwwlk2clwwlk  28615  wlkl0  28632  nvmul0or  28913  ipasslem5  29098  ipasslem11  29103  hvmul0or  29288  his6  29362  hhssnv  29527  ocsh  29546  ocin  29559  shsidmi  29647  chnlen0  29707  h1de2bi  29817  h1de2ctlem  29818  h1de2ci  29819  spansni  29820  3oalem1  29925  nmcexi  30289  atcveq0  30611  chcv1  30618  cdjreui  30695  cdj3lem2b  30700  xrge0tsmsd  31219  ccfldextdgrr  31644  ordtrest2NEWlem  31774  ordtrest2NEW  31775  xrge0iifcnv  31785  esumc  31919  esumpcvgval  31946  ballotlemfc0  32359  ballotlemfcc  32360  subfacp1lem4  33045  subfacp1lem5  33046  erdszelem8  33060  sconnpi1  33101  cvmsss2  33136  cvmlift2lem12  33176  satfv0  33220  satfv0fun  33233  satf00  33236  sat1el2xp  33241  fmla0xp  33245  fmlasucdisj  33261  satffunlem1lem1  33264  satffunlem2lem1  33266  dmopab3rexdif  33267  msubco  33393  msubvrs  33422  sinccvglem  33530  untsucf  33551  nnuni  33595  eldifsucnn  33597  eqfunresadj  33641  dfrdg2  33677  ttrcltr  33702  rnttrcl  33708  ttrclselem1  33711  frpoins3xpg  33714  frpoins3xp3g  33715  poxp2  33717  xpord2pred  33719  sexp2  33720  poxp3  33723  xpord3pred  33725  nolesgn2ores  33802  nogesgn1ores  33804  nolt02o  33825  nogt01o  33826  nosupbnd2  33846  noinfbnd2lem1  33860  noetasuplem4  33866  noetainflem4  33870  madef  33967  sltlpss  34014  lrrecfr  34027  addsval  34053  colineardim1  34290  btwnconn1lem14  34329  segleantisym  34344  colinbtwnle  34347  outsidele  34361  lineunray  34376  linethru  34382  elicc3  34433  opnregcld  34446  cldregopn  34447  fnejoin2  34485  bj-isrvec  35392  dissneqlem  35438  icorempo  35449  relowlssretop  35461  relowlpssretop  35462  rdgssun  35476  finxpsuclem  35495  lindsenlbs  35699  ptrecube  35704  poimirlem6  35710  poimirlem7  35711  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  itg2addnclem3  35757  ftc1anclem6  35782  dvasin  35788  unirep  35798  sdclem2  35827  ssbnd  35873  prdsbnd  35878  cntotbnd  35881  heibor1lem  35894  rrnequiv  35920  ismndo2  35959  grpoeqdivid  35966  isdrngo3  36044  crngohomfo  36091  0idl  36110  1idl  36111  divrngidl  36113  smprngopr  36137  prnc  36152  ispridlc  36155  riotaclbgBAD  36895  lshpdisj  36928  lsateln0  36936  lsatcveq0  36973  opnlen0  37129  cmtbr4N  37196  cvrnbtwn2  37216  cvrnbtwn4  37220  atcvreq0  37255  cvlatexch1  37277  exatleN  37345  atlelt  37379  ps-2  37419  llnn0  37457  lplnn0N  37488  islpln2a  37489  lvoln0N  37532  islvol2aN  37533  4at  37554  dalemcea  37601  dalem3  37605  pmapglb2N  37712  pmapglb2xN  37713  cdlema1N  37732  cdlemb  37735  paddasslem17  37777  llnexchb2lem  37809  llnexchb2  37810  lhpat3  37987  ltrnid  38076  trlne  38126  cdlemc4  38135  cdleme11h  38207  cdlemednuN  38241  cdlemg1a  38511  tendoeq2  38715  tendoid0  38766  dva1dim  38926  dib1dim  39106  dihlatat  39278  dochkrshp4  39330  dochkr1  39419  lclkrlem2e  39452  lcfrlem16  39499  lcfrlem28  39511  mapd0  39606  hdmap14lem13  39821  fnsnbt  40134  frlmsnic  40188  dvdsexpnn0  40262  reladdrsub  40289  sn-negex12  40319  sn-mulid2  40338  sn-mul02  40343  mulgt0con1d  40349  mulgt0con2d  40350  sn-sup2  40360  prjspner1  40384  elrfi  40432  mrefg2  40445  eldiophb  40495  eldioph2b  40501  diophin  40510  diophun  40511  rexzrexnn0  40542  eldioph4b  40549  diophren  40551  rencldnfilem  40558  pellexlem6  40572  jm2.19  40731  rmydioph  40752  expdiophlem1  40759  expdioph  40761  lnr2i  40857  lpirlnr  40858  hbtlem2  40865  hbtlem4  40867  hbtlem6  40870  dgrsub2  40876  dgraa0p  40890  rngunsnply  40914  dfsucon  41028  radcnvrat  41821  pm14.24  41939  addrcom  41982  afveu  44532  dfafn5b  44540  rlimdmafv  44556  afv2eu  44617  rlimdmafv2  44637  el1fzopredsuc  44705  elsetpreimafvssdm  44726  imasetpreimafvbijlemfo  44745  sprvalpw  44820  prprvalpw  44855  reupr  44862  fmtnofac2lem  44908  proththdlem  44953  perfectALTVlem2  45062  perfectALTV  45063  gbowpos  45099  gbowgt5  45102  gboge9  45104  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  isomuspgr  45174  lincellss  45655  lindsrng01  45697  suppdm  45739  nnpw2pb  45821  0aryfvalel  45868  0aryfvalelfv  45869  itsclc0xyqsolr  46003