Theorem syl5ibrcom 249

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  biimprcd  252  elsn2g  4597  preq1b  4771  elpreqprb  4792  reusv3  5298  alxfr  5300  reuhypd  5312  opth1  5360  euotd  5396  otiunsndisj  5403  tz7.2  5534  frsn  5634  dmopab2rex  5781  elsnxp  6137  reuop  6139  ordtri1  6219  ordtri3  6222  fvmptdv2  6781  fveqressseq  6842  foco2  6868  fsn  6892  fnsnb  6923  fmptsng  6925  fmptsnd  6926  fconst2g  6960  fnprb  6965  fntpb  6966  funfvima  6986  soisoi  7075  isores3  7082  riotaeqimp  7134  eusvobj2  7143  ovmpodv2  7302  f1opw2  7394  sorpssun  7450  sorpssin  7451  oneqmin  7514  nlimsucg  7551  onzsl  7555  tfinds  7568  funcnvuni  7630  opiota  7751  mposn  7792  suppssov1  7856  suppssfv  7860  brtpos  7895  wfrlem10  7958  wfrlem14  7962  wfrlem15  7963  seqomlem1  8080  seqomlem2  8081  omordi  8186  omord  8188  omwordi  8191  oeeui  8222  nnmordi  8251  nnmord  8252  nnmwordi  8255  nnawordex  8257  nnaordex  8258  nneob  8273  omsmolem  8274  qsss  8352  eroveu  8386  mapsncnv  8451  ralxpmap  8454  elixpsn  8495  ixpsnf1o  8496  boxcutc  8499  pw2f1olem  8615  2pwne  8667  mapxpen  8677  mapunen  8680  php  8695  unxpdomlem2  8717  en1eqsnbi  8743  isfiniteg  8772  fofinf1o  8793  f1opwfi  8822  elfiun  8888  oieu  8997  brwdom2  9031  wdomtr  9033  ixpiunwdom  9049  en3lplem1  9069  suc11reg  9076  inf3lemd  9084  cantnfvalf  9122  cantnflt  9129  cantnfp1lem3  9137  cantnflem2  9147  r1tr  9199  updjud  9357  dfac8alem  9449  wdomnumr  9484  isinfcard  9512  aceq3lem  9540  dfac5lem4  9546  dfac5  9548  dfac2b  9550  coftr  9689  fin23lem28  9756  fin23lem29  9757  fin1a2lem11  9826  fin1a2lem12  9827  fin1a2lem13  9828  hsmexlem9  9841  axdclem  9935  pwcfsdom  9999  gchdomtri  10045  fpwwe2  10059  gchpwdom  10086  gchhar  10095  addnidpi  10317  nqereu  10345  genpv  10415  genpdm  10418  distrlem5pr  10443  mulid1  10633  ltne  10731  mul02  10812  cnegex  10815  mul0or  11274  negfi  11583  sup2  11591  supaddc  11602  supadd  11603  supmul1  11604  supmul  11607  creur  11626  creui  11627  cju  11628  nnsub  11675  un0addcl  11924  un0mulcl  11925  nn0sub  11941  elz2  11993  zaddcl  12016  suprzcl2  12332  qmulz  12345  qre  12347  qnegcl  12359  elpqb  12369  xrmax1  12562  xrmin2  12565  max1ALT  12573  xlesubadd  12650  xmulass  12674  xlemul1a  12675  xrsupexmnf  12692  xrinfmexpnf  12693  xrub  12699  iccid  12777  fzsn  12943  fzsuc2  12959  fz1sbc  12977  elfzp12  12980  modmuladd  13275  seqid3  13408  bcval5  13672  bcpasc  13675  hashbnd  13690  hashnnn0genn0  13697  hashprg  13750  hashfzo  13784  wrdl1s1  13962  ccats1alpha  13967  cats1un  14077  shftlem  14421  replim  14469  absmod0  14657  absz  14665  rlimdm  14902  summolem2  15067  summo  15068  zsum  15069  fsum  15071  fsummulc2  15133  fsumconst  15139  fsum00  15147  incexclem  15185  isumsplit  15189  infcvgaux1i  15206  prodmolem2  15283  prodmo  15284  zprod  15285  fprod  15289  prodsn  15310  prodsnf  15312  fprodconst  15326  ruclem2  15579  fzo0dvdseq  15667  bitsf1ocnv  15787  sadcaddlem  15800  smueqlem  15833  gcdabs1  15872  bezoutlem1  15881  bezoutlem3  15883  bezoutlem4  15884  dvdsgcd  15886  dvdsmulgcd  15899  lcmgcdeq  15950  lcmf  15971  lcmfunsnlem1  15975  lcmfunsnlem2lem2  15977  isprm2lem  16019  dvdsprime  16025  isprm5  16045  coprm  16049  prmdvdsexpr  16055  rpexp  16058  phibndlem  16101  dfphi2  16105  hashgcdlem  16119  odzdvds  16126  nnoddn2prm  16142  pythagtriplem1  16147  iserodd  16166  pceulem  16176  pcqmul  16184  pcqcl  16187  pcxcl  16191  pcneg  16204  pcabs  16205  pcgcd1  16207  pcz  16211  pcprmpw2  16212  pcprmpw  16213  dvdsprmpweqle  16216  difsqpwdvds  16217  pcaddlem  16218  pcadd  16219  pcmpt  16222  pockthg  16236  prmreclem5  16250  4sqlem4  16282  mul4sq  16284  vdwapun  16304  vdwlem2  16312  vdwlem6  16316  vdwlem8  16318  vdwlem13  16323  0ram  16350  ram0  16352  ramcl  16359  cshwsiun  16427  wunress  16558  firest  16700  isssc  17084  pospo  17577  latnlej  17672  gsumval2a  17889  mnd1id  17947  0subm  17976  mulgnn0p1  18233  mulgnn0ass  18257  cyccom  18340  gicsubgen  18412  symg1bas  18513  snsymgefmndeq  18517  psgnunilem1  18615  psgnunilem2  18617  mndodcongi  18665  oddvdsnn0  18666  odnncl  18667  oddvds  18669  odeq  18672  odeq1  18681  pgpfi2  18725  sylow2a  18738  sylow2blem3  18741  sylow3lem6  18751  lsmelvalm  18770  lsmsubm  18772  lsmsubg  18773  lsmmod  18795  lsmdisj2  18802  efgmnvl  18834  efgtlen  18846  efgs1b  18856  efgrelexlemb  18870  efgredeu  18872  efgcpbllemb  18875  frgpuptinv  18891  frgpup3lem  18897  qusabl  18979  frgpnabllem1  18987  cyggeninv  18996  cyggenod  18997  cygablOLD  19005  gsumval3eu  19018  dprdssv  19132  dprdfeq0  19138  dprdsubg  19140  dprddisj2  19155  ablfacrp  19182  pgpfac1lem3  19193  pgpfaclem2  19198  dvreq1  19437  irredn1  19450  drngmul0or  19517  isabvd  19585  abvdom  19603  issrngd  19626  lmodfopnelem2  19665  lss1d  19729  lspsneq0  19778  lbspss  19848  lsmcl  19849  lvecvs0or  19874  lspindpi  19898  lidl1el  19985  lpiss  20017  lidldvgen  20022  nzrunit  20034  rrgeq0  20057  domneq0  20064  mplsubrglem  20213  mplmonmul  20239  mplcoe5lem  20242  coe1tmmul2  20438  coe1tmmul  20439  pf1ind  20512  qsssubdrg  20598  zringlpirlem1  20625  znfld  20701  znunit  20704  znrrg  20706  cygznlem3  20710  frgpcyg  20714  psgnghm  20718  ipeq0  20776  cssincl  20826  lsmcss  20830  obselocv  20866  dsmmacl  20879  dsmmlss  20882  mat1dimelbas  21074  mdetralt  21211  mdetunilem2  21216  mdetunilem7  21221  mdetunilem9  21223  maducoeval2  21243  chpscmat  21444  chfacfscmulgsum  21462  chfacfpmmulgsum  21466  istopon  21514  eltg3  21564  tgidm  21582  clsval2  21652  opncldf1  21686  restbas  21760  tgrest  21761  restcld  21774  restcldr  21776  restcls  21783  restntr  21784  ordtbas2  21793  ordtbas  21794  ordtrest2lem  21805  ordtrest2  21806  pnfnei  21822  mnfnei  21823  tgcn  21854  cnconst  21886  cnindis  21894  lmss  21900  ordtt1  21981  discmp  22000  1stcrest  22055  2ndcdisj  22058  cldllycmp  22097  txbas  22169  ptpjpre1  22173  ptuni2  22178  ptbasin  22179  ptbasfi  22183  ptopn2  22186  txbasval  22208  ptpjopn  22214  ptclsg  22217  dfac14lem  22219  xkoccn  22221  ptcnp  22224  upxp  22225  ptrescn  22241  txkgen  22254  xkoptsub  22256  xkopt  22257  xkoco1cn  22259  xkoco2cn  22260  xkococn  22262  xkoinjcn  22289  ordthmeolem  22403  ptuncnv  22409  nrmhaus  22428  fbssint  22440  fbfinnfr  22443  fbasrn  22486  isufil2  22510  filufint  22522  rnelfm  22555  fmfnfmlem2  22557  fmfnfmlem3  22558  fmfnfmlem4  22559  fmfnfm  22560  flimtopon  22572  flimclslem  22586  fclstopon  22614  fclscf  22627  flimfnfcls  22630  alexsublem  22646  alexsubALTlem3  22651  alexsubALTlem4  22652  ptcmplem2  22655  tmdgsum2  22698  symgtgp  22708  cldsubg  22713  qustgplem  22723  tgptsmscld  22753  tsmsxplem1  22755  imasdsf1olem  22977  blssps  23028  blss  23029  stdbdxmet  23119  methaus  23124  metrest  23128  nrginvrcn  23295  nmoeq0  23339  blssioo  23397  xrtgioo  23408  xrsxmet  23411  reconnlem1  23428  reconnlem2  23429  xrge0tsms  23436  elcncf1di  23497  iccpnfcnv  23542  evth  23557  lebnumlem1  23559  lebnumlem2  23560  lebnumlem3  23561  nmoleub3  23717  minveclem3b  24025  ivthlem2  24047  ivthlem3  24048  elovolm  24070  ovolmge0  24072  ovoliun  24100  ovolicc2lem3  24114  ovolicc2  24117  voliunlem3  24147  dyaddisj  24191  dyadmax  24193  opnmblALT  24198  ismbfd  24234  ismbf2d  24235  mbfimaopnlem  24250  mbfimaopn2  24252  i1fmullem  24289  i1fres  24300  itg1climres  24309  mbfi1fseqlem4  24313  itg2lcl  24322  itgsplitioo  24432  ellimc2  24469  rolle  24581  dvlip  24584  dvge0  24597  dvne0  24602  lhop1lem  24604  tdeglem4  24648  degltlem1  24660  deg1nn0clb  24678  deg1lt0  24679  dvdsq1p  24748  ply1rem  24751  fta1g  24755  elply2  24780  plyf  24782  ne0p  24791  plyeq0lem  24794  plypf1  24796  0dgrb  24830  coe1termlem  24842  dgrcolem2  24858  plymul0or  24864  plyrem  24888  fta1  24891  quotcan  24892  aalioulem3  24917  eff1olem  25126  lognegb  25167  eflogeq  25179  argregt0  25187  argrege0  25188  tanarg  25196  cxpexp  25245  cxpeq0  25255  mulcxp  25262  cxpeq  25332  atans2  25503  scvxcvx  25557  dmgmaddn0  25594  isppw2  25686  vmappw  25687  vmacl  25689  efvmacl  25691  isnsqf  25706  mumullem2  25751  sqff1o  25753  dvdsppwf1o  25757  ppiublem1  25772  vmalelog  25775  chtublem  25781  fsumvma  25783  perfectlem2  25800  perfect  25801  bposlem1  25854  lgsmod  25893  lgsne0  25905  lgsdirnn0  25914  lgsqr  25921  lgsdchr  25925  gausslemma2dlem1a  25935  gausslemma2dlem6  25942  lgseisenlem2  25946  lgsquadlem1  25950  lgsquadlem2  25951  2lgslem1b  25962  2sqlem2  25988  mul2sq  25989  2sqlem7  25994  dchrisum0fno1  26081  pntrsumbnd2  26137  ostthlem1  26197  ostth2lem2  26204  ostth3  26208  ostth  26209  colinearalg  26690  axpasch  26721  axlowdimlem16  26737  axlowdimlem17  26738  axlowdim  26741  axcontlem2  26745  axcontlem4  26747  axcontlem7  26750  lpvtx  26847  edglnl  26922  numedglnl  26923  usgredgop  26949  usgrexmplef  27035  uhgrspansubgrlem  27066  uhgrspan1  27079  nbusgredgeu0  27144  nb3grprlem2  27157  cusgrsize2inds  27229  vtxd0nedgb  27264  rusgrpropnb  27359  upgrwlkvtxedg  27420  wlkp1lem1  27449  wlkp1lem6  27454  wlkp1lem8  27456  usgr2wlkneq  27531  crctcshwlk  27594  crctcsh  27596  iswwlksnon  27625  wlkiswwlks1  27639  wwlksnextbi  27666  wwlksnextproplem2  27683  wspthsnonn0vne  27690  clwlkclwwlklem2  27772  clwwisshclwws  27787  erclwwlktr  27794  clwwlkel  27819  clwwlkext2edg  27829  erclwwlkntr  27844  clwlknf1oclwwlknlem2  27855  clwlknf1oclwwlknlem3  27856  clwlknf1oclwwlkn  27857  clwwlknonccat  27869  0wlkons1  27894  3wlkdlem6  27938  eupth2eucrct  27990  frgrwopreglem2  28086  2clwwlk2clwwlk  28123  wlkl0  28140  nvmul0or  28421  ipasslem5  28606  ipasslem11  28611  hvmul0or  28796  his6  28870  hhssnv  29035  ocsh  29054  ocin  29067  shsidmi  29155  chnlen0  29215  h1de2bi  29325  h1de2ctlem  29326  h1de2ci  29327  spansni  29328  3oalem1  29433  nmcexi  29797  atcveq0  30119  chcv1  30126  cdjreui  30203  cdj3lem2b  30208  xrge0tsmsd  30687  ccfldextdgrr  31052  ordtrest2NEWlem  31160  ordtrest2NEW  31161  xrge0iifcnv  31171  esumc  31305  esumpcvgval  31332  ballotlemfc0  31745  ballotlemfcc  31746  subfacp1lem4  32425  subfacp1lem5  32426  erdszelem8  32440  sconnpi1  32481  cvmsss2  32516  cvmlift2lem12  32556  satfv0  32600  satfv0fun  32613  satf00  32616  sat1el2xp  32621  fmla0xp  32625  fmlasucdisj  32641  satffunlem1lem1  32644  satffunlem2lem1  32646  dmopab3rexdif  32647  msubco  32773  msubvrs  32802  sinccvglem  32910  untsucf  32931  dfpo2  32986  eqfunresadj  32999  dfrdg2  33035  trpred0  33070  frrlem12  33129  frrlem13  33130  nolesgn2ores  33174  nolt02o  33194  nosupbnd2  33211  noetalem3  33214  colineardim1  33517  btwnconn1lem14  33556  segleantisym  33571  colinbtwnle  33574  outsidele  33588  lineunray  33603  linethru  33609  elicc3  33660  opnregcld  33673  cldregopn  33674  fnejoin2  33712  dissneqlem  34615  icorempo  34626  relowlssretop  34638  relowlpssretop  34639  rdgssun  34653  finxpsuclem  34672  lindsenlbs  34881  ptrecube  34886  poimirlem6  34892  poimirlem7  34893  poimirlem16  34902  poimirlem17  34903  poimirlem19  34905  poimirlem20  34906  poimirlem21  34907  poimirlem22  34908  poimirlem23  34909  poimirlem24  34910  poimirlem25  34911  poimirlem26  34912  poimirlem27  34913  poimirlem29  34915  poimirlem30  34916  poimirlem31  34917  poimirlem32  34918  itg2addnclem3  34939  ftc1anclem6  34966  dvasin  34972  unirep  34982  sdclem2  35011  ssbnd  35060  prdsbnd  35065  cntotbnd  35068  heibor1lem  35081  rrnequiv  35107  ismndo2  35146  grpoeqdivid  35153  isdrngo3  35231  crngohomfo  35278  0idl  35297  1idl  35298  divrngidl  35300  smprngopr  35324  prnc  35339  ispridlc  35342  riotaclbgBAD  36084  lshpdisj  36117  lsateln0  36125  lsatcveq0  36162  opnlen0  36318  cmtbr4N  36385  cvrnbtwn2  36405  cvrnbtwn4  36409  atcvreq0  36444  cvlatexch1  36466  exatleN  36534  atlelt  36568  ps-2  36608  llnn0  36646  lplnn0N  36677  islpln2a  36678  lvoln0N  36721  islvol2aN  36722  4at  36743  dalemcea  36790  dalem3  36794  pmapglb2N  36901  pmapglb2xN  36902  cdlema1N  36921  cdlemb  36924  paddasslem17  36966  llnexchb2lem  36998  llnexchb2  36999  lhpat3  37176  ltrnid  37265  trlne  37315  cdlemc4  37324  cdleme11h  37396  cdlemednuN  37430  cdlemg1a  37700  tendoeq2  37904  tendoid0  37955  dva1dim  38115  dib1dim  38295  dihlatat  38467  dochkrshp4  38519  dochkr1  38608  lclkrlem2e  38641  lcfrlem16  38688  lcfrlem28  38700  mapd0  38795  hdmap14lem13  39010  fnsnbt  39113  frlmsnic  39142  reladdrsub  39208  elrfi  39284  mrefg2  39297  eldiophb  39347  eldioph2b  39353  diophin  39362  diophun  39363  rexzrexnn0  39394  eldioph4b  39401  diophren  39403  rencldnfilem  39410  pellexlem6  39424  jm2.19  39583  rmydioph  39604  expdiophlem1  39611  expdioph  39613  lnr2i  39709  lpirlnr  39710  hbtlem2  39717  hbtlem4  39719  hbtlem6  39722  dgrsub2  39728  dgraa0p  39742  rngunsnply  39766  dfsucon  39882  radcnvrat  40639  pm14.24  40757  addrcom  40800  afveu  43345  dfafn5b  43353  rlimdmafv  43369  afv2eu  43430  rlimdmafv2  43450  el1fzopredsuc  43518  elsetpreimafvssdm  43539  imasetpreimafvbijlemfo  43558  sprvalpw  43635  prprvalpw  43670  reupr  43677  fmtnofac2lem  43723  proththdlem  43771  perfectALTVlem2  43880  perfectALTV  43881  gbowpos  43917  gbowgt5  43920  gboge9  43922  nnsum4primesodd  43954  nnsum4primesoddALTV  43955  isomuspgr  43992  lincellss  44474  lindsrng01  44516  suppdm  44558  nnpw2pb  44640  itsclc0xyqsolr  44749