Theorem syl5ibrcom 238

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

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  biimprcd  241  elsn2g  4415  preq1b  4576  elpreqprb  4601  reusv3  5087  alxfr  5089  reuhypd  5105  opth1  5146  euotd  5181  otiunsndisj  5188  tz7.2  5308  frsn  5405  elsnxp  5905  ordtri1  5983  ordtri3  5986  fvmptdv2  6529  fveqressseq  6587  foco2  6611  fsn  6635  fnsnb  6667  fmptsng  6669  fmptsnd  6670  fconst2g  6703  fnprb  6707  fntpb  6708  funfvima  6727  soisoi  6812  isores3  6819  riotaeqimp  6868  eusvobj2  6877  ovmpt2dv2  7034  f1opw2  7128  sorpssun  7184  sorpssin  7185  oneqmin  7245  nlimsucg  7282  onzsl  7286  tfinds  7299  funcnvuni  7359  opiota  7471  mpt2sn  7512  suppssov1  7572  suppssfv  7576  brtpos  7606  wfrlem10  7670  wfrlem14  7674  wfrlem15  7675  seqomlem1  7791  seqomlem2  7792  omordi  7893  omord  7895  omwordi  7898  oeeui  7929  nnmordi  7958  nnmord  7959  nnmwordi  7962  nnawordex  7964  nnaordex  7965  nneob  7979  omsmolem  7980  qsss  8053  eroveu  8088  mapsncnv  8151  ralxpmap  8154  elixpsn  8194  ixpsnf1o  8195  boxcutc  8198  pw2f1olem  8313  2pwne  8365  mapxpen  8375  mapunen  8378  php  8393  unxpdomlem2  8414  en1eqsnbi  8440  isfiniteg  8469  fofinf1o  8490  f1opwfi  8519  elfiun  8585  oieu  8693  brwdom2  8727  wdomtr  8729  ixpiunwdom  8745  en3lplem1  8764  suc11reg  8773  inf3lemd  8781  cantnfvalf  8819  cantnflt  8826  cantnfp1lem3  8834  cantnflem2  8844  r1tr  8896  updjud  9053  dfac8alem  9145  wdomnumr  9180  isinfcard  9208  aceq3lem  9236  dfac5lem4  9242  dfac5  9244  dfac2b  9246  dfac2OLD  9248  coftr  9390  fin23lem28  9457  fin23lem29  9458  fin1a2lem11  9527  fin1a2lem12  9528  fin1a2lem13  9529  hsmexlem9  9542  axdclem  9636  pwcfsdom  9700  gchdomtri  9746  fpwwe2  9760  gchpwdom  9787  gchhar  9796  addnidpi  10018  nqereu  10046  genpv  10116  genpdm  10119  distrlem5pr  10144  mulid1  10333  ltne  10429  mul02  10509  cnegex  10512  mul0or  10962  negfi  11266  sup2  11274  supaddc  11285  supadd  11286  supmul1  11287  supmul  11290  creur  11309  creui  11310  cju  11311  nnsub  11357  un0addcl  11612  un0mulcl  11613  nn0sub  11629  elz2  11680  zaddcl  11703  suprzcl2  12017  qmulz  12030  qre  12032  qnegcl  12044  xrmax1  12244  xrmin2  12247  max1ALT  12255  xlesubadd  12331  xmulass  12355  xlemul1a  12356  xrsupexmnf  12373  xrinfmexpnf  12374  xrub  12380  iccid  12458  fzsn  12626  fzsuc2  12641  fz1sbc  12659  elfzp12  12662  modmuladd  12956  seqid3  13088  bcval5  13345  bcpasc  13348  hashbnd  13363  hashnnn0genn0  13371  hashprg  13420  hashfzo  13453  wrdl1s1  13629  ccats1alpha  13634  cats1un  13719  shftlem  14051  replim  14099  absmod0  14286  absz  14294  rlimdm  14525  summolem2  14690  summo  14691  zsum  14692  fsum  14694  fsummulc2  14758  fsumconst  14764  fsum00  14772  incexclem  14810  isumsplit  14814  infcvgaux1i  14831  prodmolem2  14906  prodmo  14907  zprod  14908  fprod  14912  prodsn  14933  prodsnf  14935  fprodconst  14949  ruclem2  15201  fzo0dvdseq  15288  bitsf1ocnv  15405  sadcaddlem  15418  smueqlem  15451  gcdabs1  15490  bezoutlem1  15495  bezoutlem3  15497  bezoutlem4  15498  dvdsgcd  15500  dvdsmulgcd  15513  lcmgcdeq  15564  lcmf  15585  lcmfunsnlem1  15589  lcmfunsnlem2lem2  15591  isprm2lem  15632  dvdsprime  15638  isprm5  15656  coprm  15660  prmdvdsexpr  15666  rpexp  15669  phibndlem  15712  dfphi2  15716  hashgcdlem  15730  odzdvds  15737  nnoddn2prm  15753  pythagtriplem1  15758  iserodd  15777  pceulem  15787  pcqmul  15795  pcqcl  15798  pcxcl  15802  pcneg  15815  pcabs  15816  pcgcd1  15818  pcz  15822  pcprmpw2  15823  pcprmpw  15824  dvdsprmpweqle  15827  difsqpwdvds  15828  pcaddlem  15829  pcadd  15830  pcmpt  15833  pockthg  15847  prmreclem5  15861  4sqlem4  15893  mul4sq  15895  vdwapun  15915  vdwlem2  15923  vdwlem6  15927  vdwlem8  15929  vdwlem13  15934  0ram  15961  ram0  15963  ramcl  15970  cshwsiun  16038  wunress  16172  firest  16318  xpscfv  16447  isssc  16704  pospo  17198  latnlej  17293  gsumval2a  17504  mnd1id  17557  mulgnn0p1  17777  mulgnn0ass  17800  gicsubgen  17942  symg1bas  18037  psgnunilem1  18134  psgnunilem2  18136  mndodcongi  18183  oddvdsnn0  18184  odnncl  18185  oddvds  18187  odeq  18190  odeq1  18198  pgpfi2  18242  sylow2a  18255  sylow2blem3  18258  sylow3lem6  18268  lsmelvalm  18287  lsmsubm  18289  lsmsubg  18290  lsmmod  18309  lsmdisj2  18316  efgmnvl  18348  efgtlen  18360  efgs1b  18370  efgrelexlemb  18384  efgredeu  18386  efgcpbllemb  18389  frgpuptinv  18405  frgpup3lem  18411  qusabl  18489  frgpnabllem1  18497  cyggeninv  18506  cyggenod  18507  cygabl  18513  gsumval3eu  18526  dprdssv  18637  dprdfeq0  18643  dprdsubg  18645  dprddisj2  18660  ablfacrp  18687  pgpfac1lem3  18698  pgpfaclem2  18703  dvreq1  18915  irredn1  18928  drngmul0or  18992  isabvd  19044  abvdom  19062  issrngd  19085  lmodfopnelem2  19124  lss1d  19190  lspsneq0  19239  lbspss  19309  lsmcl  19310  lvecvs0or  19335  lspindpi  19360  lidl1el  19447  lpiss  19479  lidldvgen  19484  nzrunit  19496  rrgeq0  19519  domneq0  19526  mplsubrglem  19668  mplmonmul  19693  mplcoe5lem  19696  coe1tmmul2  19874  coe1tmmul  19875  pf1ind  19947  qsssubdrg  20033  zringlpirlem1  20060  znfld  20136  znunit  20139  znrrg  20141  cygznlem3  20145  frgpcyg  20149  psgnghm  20153  ipeq0  20213  cssincl  20263  lsmcss  20267  obselocv  20303  dsmmacl  20316  dsmmlss  20319  mat1dimelbas  20509  mdetralt  20646  mdetunilem2  20651  mdetunilem7  20656  mdetunilem9  20658  maducoeval2  20678  chpscmat  20881  chfacfscmulgsum  20899  chfacfpmmulgsum  20903  istopon  20951  eltg3  21001  tgidm  21019  clsval2  21089  opncldf1  21123  restbas  21197  tgrest  21198  restcld  21211  restcldr  21213  restcls  21220  restntr  21221  ordtbas2  21230  ordtbas  21231  ordtrest2lem  21242  ordtrest2  21243  pnfnei  21259  mnfnei  21260  tgcn  21291  cnconst  21323  cnindis  21331  lmss  21337  ordtt1  21418  discmp  21436  1stcrest  21491  2ndcdisj  21494  cldllycmp  21533  txbas  21605  ptpjpre1  21609  ptuni2  21614  ptbasin  21615  ptbasfi  21619  ptopn2  21622  txbasval  21644  ptpjopn  21650  ptclsg  21653  dfac14lem  21655  xkoccn  21657  ptcnp  21660  upxp  21661  ptrescn  21677  txkgen  21690  xkoptsub  21692  xkopt  21693  xkoco1cn  21695  xkoco2cn  21696  xkococn  21698  xkoinjcn  21725  ordthmeolem  21839  ptuncnv  21845  nrmhaus  21864  fbssint  21876  fbfinnfr  21879  fbasrn  21922  isufil2  21946  filufint  21958  rnelfm  21991  fmfnfmlem2  21993  fmfnfmlem3  21994  fmfnfmlem4  21995  fmfnfm  21996  flimtopon  22008  flimclslem  22022  fclstopon  22050  fclscf  22063  flimfnfcls  22066  alexsublem  22082  alexsubALTlem3  22087  alexsubALTlem4  22088  ptcmplem2  22091  tmdgsum2  22134  symgtgp  22139  cldsubg  22148  qustgplem  22158  tgptsmscld  22188  tsmsxplem1  22190  imasdsf1olem  22412  blssps  22463  blss  22464  stdbdxmet  22554  methaus  22559  metrest  22563  nrginvrcn  22730  nmoeq0  22774  blssioo  22832  xrtgioo  22843  xrsxmet  22846  reconnlem1  22863  reconnlem2  22864  xrge0tsms  22871  elcncf1di  22932  iccpnfcnv  22977  evth  22992  lebnumlem1  22994  lebnumlem2  22995  lebnumlem3  22996  nmoleub3  23152  minveclem3b  23434  ivthlem2  23456  ivthlem3  23457  elovolm  23479  ovolmge0  23481  ovoliun  23509  ovolicc2lem3  23523  ovolicc2  23526  voliunlem3  23556  dyaddisj  23600  dyadmax  23602  opnmblALT  23607  ismbfd  23643  ismbf2d  23644  mbfimaopnlem  23659  mbfimaopn2  23661  i1fmullem  23698  i1fres  23709  itg1climres  23718  mbfi1fseqlem4  23722  itg2lcl  23731  itgsplitioo  23841  ellimc2  23878  rolle  23990  dvlip  23993  dvge0  24006  dvne0  24011  lhop1lem  24013  tdeglem4  24057  degltlem1  24069  deg1nn0clb  24087  deg1lt0  24088  dvdsq1p  24157  ply1rem  24160  fta1g  24164  elply2  24189  plyf  24191  ne0p  24200  plyeq0lem  24203  plypf1  24205  0dgrb  24239  coe1termlem  24251  dgrcolem2  24267  plymul0or  24273  plyrem  24297  fta1  24300  quotcan  24301  aalioulem3  24326  eff1olem  24532  lognegb  24573  eflogeq  24585  argregt0  24593  argrege0  24594  tanarg  24602  cxpexp  24651  cxpeq0  24661  mulcxp  24668  cxpeq  24735  atans2  24895  scvxcvx  24949  dmgmaddn0  24986  isppw2  25078  vmappw  25079  vmacl  25081  efvmacl  25083  isnsqf  25098  mumullem2  25143  sqff1o  25145  dvdsppwf1o  25149  ppiublem1  25164  vmalelog  25167  chtublem  25173  fsumvma  25175  perfectlem2  25192  perfect  25193  bposlem1  25246  lgsmod  25285  lgsne0  25297  lgsdirnn0  25306  lgsqr  25313  lgsdchr  25317  gausslemma2dlem1a  25327  gausslemma2dlem6  25334  lgseisenlem2  25338  lgsquadlem1  25342  lgsquadlem2  25343  2lgslem1b  25354  2sqlem2  25380  mul2sq  25381  2sqlem7  25386  dchrisum0fno1  25437  pntrsumbnd2  25493  ostthlem1  25553  ostth2lem2  25560  ostth3  25564  ostth  25565  colinearalg  26027  axpasch  26058  axlowdimlem16  26074  axlowdimlem17  26075  axlowdim  26078  axcontlem2  26082  axcontlem4  26084  axcontlem7  26087  lpvtx  26200  edglnl  26276  numedglnl  26277  usgredgop  26303  usgrexmplef  26390  uhgrspansubgrlem  26421  uhgrspan1  26434  nbusgredgeu0  26509  nb3grprlem2  26522  cusgrsize2inds  26600  vtxd0nedgb  26635  rusgrpropnb  26730  upgrwlkvtxedg  26792  wlkp1lem1  26821  wlkp1lem6  26826  wlkp1lem8  26828  usgr2wlkneq  26903  crctcshwlk  26966  crctcsh  26968  iswwlksnon  26998  wlkiswwlks1  27017  wlkwwlksurOLD  27048  wwlksnextbi  27054  wwlksnextproplem2  27071  wspthsnonn0vne  27080  clwlkclwwlklem2  27166  clwwisshclwws  27181  erclwwlktr  27188  clwwlkext2edg  27229  erclwwlkntr  27245  clwlksfclwwlk1hashOLD  27257  clwlknf1oclwwlknlem2  27269  clwlknf1oclwwlknlem3  27270  clwlknf1oclwwlkn  27271  clwwlknonccat  27287  0wlkons1  27317  3wlkdlem6  27361  eupth2eucrct  27413  frgrwopreglem2  27511  2clwwlk2clwwlk  27550  wlkl0  27570  nvmul0or  27856  ipasslem5  28041  ipasslem11  28046  hvmul0or  28233  his6  28307  hhssnv  28472  ocsh  28493  ocin  28506  shsidmi  28594  chnlen0  28654  h1de2bi  28764  h1de2ctlem  28765  h1de2ci  28766  spansni  28767  3oalem1  28872  nmcexi  29236  atcveq0  29558  chcv1  29565  cdjreui  29642  cdj3lem2b  29647  xrge0tsmsd  30133  ordtrest2NEWlem  30316  ordtrest2NEW  30317  xrge0iifcnv  30327  esumc  30461  esumpcvgval  30488  ballotlemfc0  30902  ballotlemfcc  30903  subfacp1lem4  31510  subfacp1lem5  31511  erdszelem8  31525  sconnpi1  31566  cvmsss2  31601  cvmlift2lem12  31641  msubco  31773  msubvrs  31802  sinccvglem  31910  untsucf  31931  dfpo2  31989  eqfunresadj  32003  dfrdg2  32043  trpred0  32078  nolesgn2ores  32168  nolt02o  32188  nosupbnd2  32205  noetalem3  32208  colineardim1  32511  btwnconn1lem14  32550  segleantisym  32565  colinbtwnle  32568  outsidele  32582  lineunray  32597  linethru  32603  elicc3  32654  opnregcld  32668  cldregopn  32669  fnejoin2  32707  dissneqlem  33523  icorempt2  33534  relowlssretop  33546  relowlpssretop  33547  finxpsuclem  33569  lindsenlbs  33736  ptrecube  33741  poimirlem6  33747  poimirlem7  33748  poimirlem16  33757  poimirlem17  33758  poimirlem19  33760  poimirlem20  33761  poimirlem21  33762  poimirlem22  33763  poimirlem23  33764  poimirlem24  33765  poimirlem25  33766  poimirlem26  33767  poimirlem27  33768  poimirlem29  33770  poimirlem30  33771  poimirlem31  33772  poimirlem32  33773  itg2addnclem3  33794  ftc1anclem6  33821  dvasin  33827  unirep  33838  sdclem2  33868  ssbnd  33917  prdsbnd  33922  cntotbnd  33925  heibor1lem  33938  rrnequiv  33964  ismndo2  34003  grpoeqdivid  34010  isdrngo3  34088  crngohomfo  34135  0idl  34154  1idl  34155  divrngidl  34157  smprngopr  34181  prnc  34196  ispridlc  34199  riotaclbgBAD  34752  lshpdisj  34786  lsateln0  34794  lsatcveq0  34831  opnlen0  34987  cmtbr4N  35054  cvrnbtwn2  35074  cvrnbtwn4  35078  atcvreq0  35113  cvlatexch1  35135  exatleN  35203  atlelt  35237  ps-2  35277  llnn0  35315  lplnn0N  35346  islpln2a  35347  lvoln0N  35390  islvol2aN  35391  4at  35412  dalemcea  35459  dalem3  35463  pmapglb2N  35570  pmapglb2xN  35571  cdlema1N  35590  cdlemb  35593  paddasslem17  35635  llnexchb2lem  35667  llnexchb2  35668  lhpat3  35845  ltrnid  35934  trlne  35984  cdlemc4  35993  cdleme11h  36065  cdlemednuN  36099  cdlemg1a  36369  tendoeq2  36573  tendoid0  36624  dva1dim  36784  dib1dim  36964  dihlatat  37136  dochkrshp4  37188  dochkr1  37277  lclkrlem2e  37310  lcfrlem16  37357  lcfrlem28  37369  mapd0  37464  hdmap14lem13  37679  elrfi  37777  mrefg2  37790  eldiophb  37840  eldioph2b  37846  diophin  37856  diophun  37857  rexzrexnn0  37888  eldioph4b  37895  diophren  37897  rencldnfilem  37904  pellexlem6  37918  jm2.19  38079  rmydioph  38100  expdiophlem1  38107  expdioph  38109  lnr2i  38205  lpirlnr  38206  hbtlem2  38213  hbtlem4  38215  hbtlem6  38218  dgrsub2  38224  dgraa0p  38238  rngunsnply  38262  radcnvrat  39031  pm14.24  39150  addrcom  39195  afveu  41760  dfafn5b  41768  rlimdmafv  41784  afv2eu  41845  rlimdmafv2  41865  el1fzopredsuc  41928  fmtnofac2lem  42073  proththdlem  42123  perfectALTVlem2  42224  perfectALTV  42225  gbowpos  42240  gbowgt5  42243  gboge9  42245  nnsum4primesodd  42277  nnsum4primesoddALTV  42278  sprvalpw  42316  lincellss  42801  lindsrng01  42843  suppdm  42886  nnpw2pb  42967