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  4603  preq1b  4777  elpreqprb  4798  reusv3  5306  alxfr  5308  reuhypd  5320  opth1  5367  euotd  5403  otiunsndisj  5410  tz7.2  5539  frsn  5639  dmopab2rex  5786  elsnxp  6142  reuop  6144  ordtri1  6224  ordtri3  6227  fvmptdv2  6786  fveqressseq  6847  foco2  6873  fsn  6897  fnsnb  6928  fmptsng  6930  fmptsnd  6931  fconst2g  6965  fnprb  6971  fntpb  6972  funfvima  6992  soisoi  7081  isores3  7088  riotaeqimp  7140  eusvobj2  7149  ovmpodv2  7308  f1opw2  7400  sorpssun  7456  sorpssin  7457  oneqmin  7520  nlimsucg  7557  onzsl  7561  tfinds  7574  funcnvuni  7636  opiota  7757  mposn  7798  suppssov1  7862  suppssfv  7866  brtpos  7901  wfrlem10  7964  wfrlem14  7968  wfrlem15  7969  seqomlem1  8086  seqomlem2  8087  omordi  8192  omord  8194  omwordi  8197  oeeui  8228  nnmordi  8257  nnmord  8258  nnmwordi  8261  nnawordex  8263  nnaordex  8264  nneob  8279  omsmolem  8280  qsss  8358  eroveu  8392  mapsncnv  8457  ralxpmap  8460  elixpsn  8501  ixpsnf1o  8502  boxcutc  8505  pw2f1olem  8621  2pwne  8673  mapxpen  8683  mapunen  8686  php  8701  unxpdomlem2  8723  en1eqsnbi  8749  isfiniteg  8778  fofinf1o  8799  f1opwfi  8828  elfiun  8894  oieu  9003  brwdom2  9037  wdomtr  9039  ixpiunwdom  9055  en3lplem1  9075  suc11reg  9082  inf3lemd  9090  cantnfvalf  9128  cantnflt  9135  cantnfp1lem3  9143  cantnflem2  9153  r1tr  9205  updjud  9363  dfac8alem  9455  wdomnumr  9490  isinfcard  9518  aceq3lem  9546  dfac5lem4  9552  dfac5  9554  dfac2b  9556  coftr  9695  fin23lem28  9762  fin23lem29  9763  fin1a2lem11  9832  fin1a2lem12  9833  fin1a2lem13  9834  hsmexlem9  9847  axdclem  9941  pwcfsdom  10005  gchdomtri  10051  fpwwe2  10065  gchpwdom  10092  gchhar  10101  addnidpi  10323  nqereu  10351  genpv  10421  genpdm  10424  distrlem5pr  10449  mulid1  10639  ltne  10737  mul02  10818  cnegex  10821  mul0or  11280  negfi  11589  sup2  11597  supaddc  11608  supadd  11609  supmul1  11610  supmul  11613  creur  11632  creui  11633  cju  11634  nnsub  11682  un0addcl  11931  un0mulcl  11932  nn0sub  11948  elz2  12000  zaddcl  12023  suprzcl2  12339  qmulz  12352  qre  12354  qnegcl  12366  elpqb  12376  xrmax1  12569  xrmin2  12572  max1ALT  12580  xlesubadd  12657  xmulass  12681  xlemul1a  12682  xrsupexmnf  12699  xrinfmexpnf  12700  xrub  12706  iccid  12784  fzsn  12950  fzsuc2  12966  fz1sbc  12984  elfzp12  12987  modmuladd  13282  seqid3  13415  bcval5  13679  bcpasc  13682  hashbnd  13697  hashnnn0genn0  13704  hashprg  13757  hashfzo  13791  wrdl1s1  13968  ccats1alpha  13973  cats1un  14083  shftlem  14427  replim  14475  absmod0  14663  absz  14671  rlimdm  14908  summolem2  15073  summo  15074  zsum  15075  fsum  15077  fsummulc2  15139  fsumconst  15145  fsum00  15153  incexclem  15191  isumsplit  15195  infcvgaux1i  15212  prodmolem2  15289  prodmo  15290  zprod  15291  fprod  15295  prodsn  15316  prodsnf  15318  fprodconst  15332  ruclem2  15585  fzo0dvdseq  15673  bitsf1ocnv  15793  sadcaddlem  15806  smueqlem  15839  gcdabs1  15878  bezoutlem1  15887  bezoutlem3  15889  bezoutlem4  15890  dvdsgcd  15892  dvdsmulgcd  15905  lcmgcdeq  15956  lcmf  15977  lcmfunsnlem1  15981  lcmfunsnlem2lem2  15983  isprm2lem  16025  dvdsprime  16031  isprm5  16051  coprm  16055  prmdvdsexpr  16061  rpexp  16064  phibndlem  16107  dfphi2  16111  hashgcdlem  16125  odzdvds  16132  nnoddn2prm  16148  pythagtriplem1  16153  iserodd  16172  pceulem  16182  pcqmul  16190  pcqcl  16193  pcxcl  16197  pcneg  16210  pcabs  16211  pcgcd1  16213  pcz  16217  pcprmpw2  16218  pcprmpw  16219  dvdsprmpweqle  16222  difsqpwdvds  16223  pcaddlem  16224  pcadd  16225  pcmpt  16228  pockthg  16242  prmreclem5  16256  4sqlem4  16288  mul4sq  16290  vdwapun  16310  vdwlem2  16318  vdwlem6  16322  vdwlem8  16324  vdwlem13  16329  0ram  16356  ram0  16358  ramcl  16365  cshwsiun  16433  wunress  16564  firest  16706  isssc  17090  pospo  17583  latnlej  17678  gsumval2a  17895  mnd1id  17953  0subm  17982  mulgnn0p1  18239  mulgnn0ass  18263  cyccom  18346  gicsubgen  18418  symg1bas  18519  snsymgefmndeq  18523  psgnunilem1  18621  psgnunilem2  18623  mndodcongi  18671  oddvdsnn0  18672  odnncl  18673  oddvds  18675  odeq  18678  odeq1  18687  pgpfi2  18731  sylow2a  18744  sylow2blem3  18747  sylow3lem6  18757  lsmelvalm  18776  lsmsubm  18778  lsmsubg  18779  lsmmod  18801  lsmdisj2  18808  efgmnvl  18840  efgtlen  18852  efgs1b  18862  efgrelexlemb  18876  efgredeu  18878  efgcpbllemb  18881  frgpuptinv  18897  frgpup3lem  18903  qusabl  18985  frgpnabllem1  18993  cyggeninv  19002  cyggenod  19003  cygablOLD  19011  gsumval3eu  19024  dprdssv  19138  dprdfeq0  19144  dprdsubg  19146  dprddisj2  19161  ablfacrp  19188  pgpfac1lem3  19199  pgpfaclem2  19204  dvreq1  19443  irredn1  19456  drngmul0or  19523  isabvd  19591  abvdom  19609  issrngd  19632  lmodfopnelem2  19671  lss1d  19735  lspsneq0  19784  lbspss  19854  lsmcl  19855  lvecvs0or  19880  lspindpi  19904  lidl1el  19991  lpiss  20023  lidldvgen  20028  nzrunit  20040  rrgeq0  20063  domneq0  20070  mplsubrglem  20219  mplmonmul  20245  mplcoe5lem  20248  coe1tmmul2  20444  coe1tmmul  20445  pf1ind  20518  qsssubdrg  20604  zringlpirlem1  20631  znfld  20707  znunit  20710  znrrg  20712  cygznlem3  20716  frgpcyg  20720  psgnghm  20724  ipeq0  20782  cssincl  20832  lsmcss  20836  obselocv  20872  dsmmacl  20885  dsmmlss  20888  mat1dimelbas  21080  mdetralt  21217  mdetunilem2  21222  mdetunilem7  21227  mdetunilem9  21229  maducoeval2  21249  chpscmat  21450  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  istopon  21520  eltg3  21570  tgidm  21588  clsval2  21658  opncldf1  21692  restbas  21766  tgrest  21767  restcld  21780  restcldr  21782  restcls  21789  restntr  21790  ordtbas2  21799  ordtbas  21800  ordtrest2lem  21811  ordtrest2  21812  pnfnei  21828  mnfnei  21829  tgcn  21860  cnconst  21892  cnindis  21900  lmss  21906  ordtt1  21987  discmp  22006  1stcrest  22061  2ndcdisj  22064  cldllycmp  22103  txbas  22175  ptpjpre1  22179  ptuni2  22184  ptbasin  22185  ptbasfi  22189  ptopn2  22192  txbasval  22214  ptpjopn  22220  ptclsg  22223  dfac14lem  22225  xkoccn  22227  ptcnp  22230  upxp  22231  ptrescn  22247  txkgen  22260  xkoptsub  22262  xkopt  22263  xkoco1cn  22265  xkoco2cn  22266  xkococn  22268  xkoinjcn  22295  ordthmeolem  22409  ptuncnv  22415  nrmhaus  22434  fbssint  22446  fbfinnfr  22449  fbasrn  22492  isufil2  22516  filufint  22528  rnelfm  22561  fmfnfmlem2  22563  fmfnfmlem3  22564  fmfnfmlem4  22565  fmfnfm  22566  flimtopon  22578  flimclslem  22592  fclstopon  22620  fclscf  22633  flimfnfcls  22636  alexsublem  22652  alexsubALTlem3  22657  alexsubALTlem4  22658  ptcmplem2  22661  tmdgsum2  22704  symgtgp  22714  cldsubg  22719  qustgplem  22729  tgptsmscld  22759  tsmsxplem1  22761  imasdsf1olem  22983  blssps  23034  blss  23035  stdbdxmet  23125  methaus  23130  metrest  23134  nrginvrcn  23301  nmoeq0  23345  blssioo  23403  xrtgioo  23414  xrsxmet  23417  reconnlem1  23434  reconnlem2  23435  xrge0tsms  23442  elcncf1di  23503  iccpnfcnv  23548  evth  23563  lebnumlem1  23565  lebnumlem2  23566  lebnumlem3  23567  nmoleub3  23723  minveclem3b  24031  ivthlem2  24053  ivthlem3  24054  elovolm  24076  ovolmge0  24078  ovoliun  24106  ovolicc2lem3  24120  ovolicc2  24123  voliunlem3  24153  dyaddisj  24197  dyadmax  24199  opnmblALT  24204  ismbfd  24240  ismbf2d  24241  mbfimaopnlem  24256  mbfimaopn2  24258  i1fmullem  24295  i1fres  24306  itg1climres  24315  mbfi1fseqlem4  24319  itg2lcl  24328  itgsplitioo  24438  ellimc2  24475  rolle  24587  dvlip  24590  dvge0  24603  dvne0  24608  lhop1lem  24610  tdeglem4  24654  degltlem1  24666  deg1nn0clb  24684  deg1lt0  24685  dvdsq1p  24754  ply1rem  24757  fta1g  24761  elply2  24786  plyf  24788  ne0p  24797  plyeq0lem  24800  plypf1  24802  0dgrb  24836  coe1termlem  24848  dgrcolem2  24864  plymul0or  24870  plyrem  24894  fta1  24897  quotcan  24898  aalioulem3  24923  eff1olem  25132  lognegb  25173  eflogeq  25185  argregt0  25193  argrege0  25194  tanarg  25202  cxpexp  25251  cxpeq0  25261  mulcxp  25268  cxpeq  25338  atans2  25509  scvxcvx  25563  dmgmaddn0  25600  isppw2  25692  vmappw  25693  vmacl  25695  efvmacl  25697  isnsqf  25712  mumullem2  25757  sqff1o  25759  dvdsppwf1o  25763  ppiublem1  25778  vmalelog  25781  chtublem  25787  fsumvma  25789  perfectlem2  25806  perfect  25807  bposlem1  25860  lgsmod  25899  lgsne0  25911  lgsdirnn0  25920  lgsqr  25927  lgsdchr  25931  gausslemma2dlem1a  25941  gausslemma2dlem6  25948  lgseisenlem2  25952  lgsquadlem1  25956  lgsquadlem2  25957  2lgslem1b  25968  2sqlem2  25994  mul2sq  25995  2sqlem7  26000  dchrisum0fno1  26087  pntrsumbnd2  26143  ostthlem1  26203  ostth2lem2  26210  ostth3  26214  ostth  26215  colinearalg  26696  axpasch  26727  axlowdimlem16  26743  axlowdimlem17  26744  axlowdim  26747  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  lpvtx  26853  edglnl  26928  numedglnl  26929  usgredgop  26955  usgrexmplef  27041  uhgrspansubgrlem  27072  uhgrspan1  27085  nbusgredgeu0  27150  nb3grprlem2  27163  cusgrsize2inds  27235  vtxd0nedgb  27270  rusgrpropnb  27365  upgrwlkvtxedg  27426  wlkp1lem1  27455  wlkp1lem6  27460  wlkp1lem8  27462  usgr2wlkneq  27537  crctcshwlk  27600  crctcsh  27602  iswwlksnon  27631  wlkiswwlks1  27645  wwlksnextbi  27672  wwlksnextproplem2  27689  wspthsnonn0vne  27696  clwlkclwwlklem2  27778  clwwisshclwws  27793  erclwwlktr  27800  clwwlkel  27825  clwwlkext2edg  27835  erclwwlkntr  27850  clwlknf1oclwwlknlem2  27861  clwlknf1oclwwlknlem3  27862  clwlknf1oclwwlkn  27863  clwwlknonccat  27875  0wlkons1  27900  3wlkdlem6  27944  eupth2eucrct  27996  frgrwopreglem2  28092  2clwwlk2clwwlk  28129  wlkl0  28146  nvmul0or  28427  ipasslem5  28612  ipasslem11  28617  hvmul0or  28802  his6  28876  hhssnv  29041  ocsh  29060  ocin  29073  shsidmi  29161  chnlen0  29221  h1de2bi  29331  h1de2ctlem  29332  h1de2ci  29333  spansni  29334  3oalem1  29439  nmcexi  29803  atcveq0  30125  chcv1  30132  cdjreui  30209  cdj3lem2b  30214  xrge0tsmsd  30692  ccfldextdgrr  31057  ordtrest2NEWlem  31165  ordtrest2NEW  31166  xrge0iifcnv  31176  esumc  31310  esumpcvgval  31337  ballotlemfc0  31750  ballotlemfcc  31751  subfacp1lem4  32430  subfacp1lem5  32431  erdszelem8  32445  sconnpi1  32486  cvmsss2  32521  cvmlift2lem12  32561  satfv0  32605  satfv0fun  32618  satf00  32621  sat1el2xp  32626  fmla0xp  32630  fmlasucdisj  32646  satffunlem1lem1  32649  satffunlem2lem1  32651  dmopab3rexdif  32652  msubco  32778  msubvrs  32807  sinccvglem  32915  untsucf  32936  dfpo2  32991  eqfunresadj  33004  dfrdg2  33040  trpred0  33075  frrlem12  33134  frrlem13  33135  nolesgn2ores  33179  nolt02o  33199  nosupbnd2  33216  noetalem3  33219  colineardim1  33522  btwnconn1lem14  33561  segleantisym  33576  colinbtwnle  33579  outsidele  33593  lineunray  33608  linethru  33614  elicc3  33665  opnregcld  33678  cldregopn  33679  fnejoin2  33717  dissneqlem  34624  icorempo  34635  relowlssretop  34647  relowlpssretop  34648  rdgssun  34662  finxpsuclem  34681  lindsenlbs  34902  ptrecube  34907  poimirlem6  34913  poimirlem7  34914  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  itg2addnclem3  34960  ftc1anclem6  34987  dvasin  34993  unirep  35003  sdclem2  35032  ssbnd  35081  prdsbnd  35086  cntotbnd  35089  heibor1lem  35102  rrnequiv  35128  ismndo2  35167  grpoeqdivid  35174  isdrngo3  35252  crngohomfo  35299  0idl  35318  1idl  35319  divrngidl  35321  smprngopr  35345  prnc  35360  ispridlc  35363  riotaclbgBAD  36105  lshpdisj  36138  lsateln0  36146  lsatcveq0  36183  opnlen0  36339  cmtbr4N  36406  cvrnbtwn2  36426  cvrnbtwn4  36430  atcvreq0  36465  cvlatexch1  36487  exatleN  36555  atlelt  36589  ps-2  36629  llnn0  36667  lplnn0N  36698  islpln2a  36699  lvoln0N  36742  islvol2aN  36743  4at  36764  dalemcea  36811  dalem3  36815  pmapglb2N  36922  pmapglb2xN  36923  cdlema1N  36942  cdlemb  36945  paddasslem17  36987  llnexchb2lem  37019  llnexchb2  37020  lhpat3  37197  ltrnid  37286  trlne  37336  cdlemc4  37345  cdleme11h  37417  cdlemednuN  37451  cdlemg1a  37721  tendoeq2  37925  tendoid0  37976  dva1dim  38136  dib1dim  38316  dihlatat  38488  dochkrshp4  38540  dochkr1  38629  lclkrlem2e  38662  lcfrlem16  38709  lcfrlem28  38721  mapd0  38816  hdmap14lem13  39031  fnsnbt  39169  frlmsnic  39198  reladdrsub  39264  elrfi  39340  mrefg2  39353  eldiophb  39403  eldioph2b  39409  diophin  39418  diophun  39419  rexzrexnn0  39450  eldioph4b  39457  diophren  39459  rencldnfilem  39466  pellexlem6  39480  jm2.19  39639  rmydioph  39660  expdiophlem1  39667  expdioph  39669  lnr2i  39765  lpirlnr  39766  hbtlem2  39773  hbtlem4  39775  hbtlem6  39778  dgrsub2  39784  dgraa0p  39798  rngunsnply  39822  dfsucon  39938  radcnvrat  40695  pm14.24  40813  addrcom  40856  afveu  43401  dfafn5b  43409  rlimdmafv  43425  afv2eu  43486  rlimdmafv2  43506  el1fzopredsuc  43574  elsetpreimafvssdm  43595  imasetpreimafvbijlemfo  43614  sprvalpw  43691  prprvalpw  43726  reupr  43733  fmtnofac2lem  43779  proththdlem  43827  perfectALTVlem2  43936  perfectALTV  43937  gbowpos  43973  gbowgt5  43976  gboge9  43978  nnsum4primesodd  44010  nnsum4primesoddALTV  44011  isomuspgr  44048  lincellss  44530  lindsrng01  44572  suppdm  44614  nnpw2pb  44696  itsclc0xyqsolr  44805