Theorem syl5ibrcom 239

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  biimprcd  242  elsn2g  4475  preq1b  4651  elpreqprb  4672  reusv3  5159  alxfr  5161  reuhypd  5176  opth1  5224  euotd  5259  otiunsndisj  5266  tz7.2  5391  frsn  5489  elsnxp  5980  reuop  5982  ordtri1  6062  ordtri3  6065  fvmptdv2  6612  fveqressseq  6672  foco2  6696  fsn  6720  fnsnb  6751  fmptsng  6753  fmptsnd  6754  fconst2g  6792  fnprb  6797  fntpb  6798  funfvima  6818  soisoi  6904  isores3  6911  riotaeqimp  6960  eusvobj2  6969  ovmpodv2  7124  f1opw2  7218  sorpssun  7274  sorpssin  7275  oneqmin  7336  nlimsucg  7373  onzsl  7377  tfinds  7390  funcnvuni  7451  opiota  7565  mposn  7606  suppssov1  7665  suppssfv  7669  brtpos  7704  wfrlem10  7768  wfrlem14  7772  wfrlem15  7773  seqomlem1  7889  seqomlem2  7890  omordi  7993  omord  7995  omwordi  7998  oeeui  8029  nnmordi  8058  nnmord  8059  nnmwordi  8062  nnawordex  8064  nnaordex  8065  nneob  8079  omsmolem  8080  qsss  8158  eroveu  8192  mapsncnv  8255  ralxpmap  8258  elixpsn  8298  ixpsnf1o  8299  boxcutc  8302  pw2f1olem  8417  2pwne  8469  mapxpen  8479  mapunen  8482  php  8497  unxpdomlem2  8518  en1eqsnbi  8544  isfiniteg  8573  fofinf1o  8594  f1opwfi  8623  elfiun  8689  oieu  8798  brwdom2  8832  wdomtr  8834  ixpiunwdom  8850  en3lplem1  8869  suc11reg  8876  inf3lemd  8884  cantnfvalf  8922  cantnflt  8929  cantnfp1lem3  8937  cantnflem2  8947  r1tr  8999  updjud  9157  dfac8alem  9249  wdomnumr  9284  isinfcard  9312  aceq3lem  9340  dfac5lem4  9346  dfac5  9348  dfac2b  9350  coftr  9493  fin23lem28  9560  fin23lem29  9561  fin1a2lem11  9630  fin1a2lem12  9631  fin1a2lem13  9632  hsmexlem9  9645  axdclem  9739  pwcfsdom  9803  gchdomtri  9849  fpwwe2  9863  gchpwdom  9890  gchhar  9899  addnidpi  10121  nqereu  10149  genpv  10219  genpdm  10222  distrlem5pr  10247  mulid1  10437  ltne  10537  mul02  10618  cnegex  10621  mul0or  11081  negfi  11390  sup2  11398  supaddc  11409  supadd  11410  supmul1  11411  supmul  11414  creur  11433  creui  11434  cju  11435  nnsub  11484  un0addcl  11742  un0mulcl  11743  nn0sub  11759  elz2  11811  zaddcl  11835  suprzcl2  12152  qmulz  12165  qre  12167  qnegcl  12180  elpqb  12190  xrmax1  12385  xrmin2  12388  max1ALT  12396  xlesubadd  12472  xmulass  12496  xlemul1a  12497  xrsupexmnf  12514  xrinfmexpnf  12515  xrub  12521  iccid  12599  fzsn  12765  fzsuc2  12781  fz1sbc  12799  elfzp12  12802  modmuladd  13096  seqid3  13229  bcval5  13493  bcpasc  13496  hashbnd  13511  hashnnn0genn0  13518  hashprg  13569  hashfzo  13603  wrdl1s1  13777  ccats1alpha  13782  cats1un  13914  shftlem  14288  replim  14336  absmod0  14524  absz  14532  rlimdm  14769  summolem2  14933  summo  14934  zsum  14935  fsum  14937  fsummulc2  14999  fsumconst  15005  fsum00  15013  incexclem  15051  isumsplit  15055  infcvgaux1i  15072  prodmolem2  15149  prodmo  15150  zprod  15151  fprod  15155  prodsn  15176  prodsnf  15178  fprodconst  15192  ruclem2  15445  fzo0dvdseq  15533  bitsf1ocnv  15653  sadcaddlem  15666  smueqlem  15699  gcdabs1  15738  bezoutlem1  15743  bezoutlem3  15745  bezoutlem4  15746  dvdsgcd  15748  dvdsmulgcd  15761  lcmgcdeq  15812  lcmf  15833  lcmfunsnlem1  15837  lcmfunsnlem2lem2  15839  isprm2lem  15881  dvdsprime  15887  isprm5  15907  coprm  15911  prmdvdsexpr  15917  rpexp  15920  phibndlem  15963  dfphi2  15967  hashgcdlem  15981  odzdvds  15988  nnoddn2prm  16004  pythagtriplem1  16009  iserodd  16028  pceulem  16038  pcqmul  16046  pcqcl  16049  pcxcl  16053  pcneg  16066  pcabs  16067  pcgcd1  16069  pcz  16073  pcprmpw2  16074  pcprmpw  16075  dvdsprmpweqle  16078  difsqpwdvds  16079  pcaddlem  16080  pcadd  16081  pcmpt  16084  pockthg  16098  prmreclem5  16112  4sqlem4  16144  mul4sq  16146  vdwapun  16166  vdwlem2  16174  vdwlem6  16178  vdwlem8  16180  vdwlem13  16185  0ram  16212  ram0  16214  ramcl  16221  cshwsiun  16289  wunress  16420  firest  16562  xpscfv  16691  isssc  16948  pospo  17441  latnlej  17536  gsumval2a  17747  mnd1id  17800  mulgnn0p1  18024  mulgnn0ass  18047  gicsubgen  18189  symg1bas  18285  psgnunilem1  18382  psgnunilem2  18385  mndodcongi  18433  oddvdsnn0  18434  odnncl  18435  oddvds  18437  odeq  18440  odeq1  18448  pgpfi2  18492  sylow2a  18505  sylow2blem3  18508  sylow3lem6  18518  lsmelvalm  18537  lsmsubm  18539  lsmsubg  18540  lsmmod  18559  lsmdisj2  18566  efgmnvl  18598  efgtlen  18610  efgs1b  18620  efgrelexlemb  18636  efgredeu  18638  efgcpbllemb  18641  frgpuptinv  18657  frgpup3lem  18663  qusabl  18741  frgpnabllem1  18749  cyggeninv  18758  cyggenod  18759  cygabl  18765  gsumval3eu  18778  dprdssv  18888  dprdfeq0  18894  dprdsubg  18896  dprddisj2  18911  ablfacrp  18938  pgpfac1lem3  18949  pgpfaclem2  18954  dvreq1  19166  irredn1  19179  drngmul0or  19246  isabvd  19313  abvdom  19331  issrngd  19354  lmodfopnelem2  19393  lss1d  19457  lspsneq0  19506  lbspss  19576  lsmcl  19577  lvecvs0or  19602  lspindpi  19626  lidl1el  19712  lpiss  19744  lidldvgen  19749  nzrunit  19761  rrgeq0  19784  domneq0  19791  mplsubrglem  19933  mplmonmul  19958  mplcoe5lem  19961  coe1tmmul2  20147  coe1tmmul  20148  pf1ind  20220  qsssubdrg  20306  zringlpirlem1  20333  znfld  20409  znunit  20412  znrrg  20414  cygznlem3  20418  frgpcyg  20422  psgnghm  20426  ipeq0  20484  cssincl  20534  lsmcss  20538  obselocv  20574  dsmmacl  20587  dsmmlss  20590  mat1dimelbas  20784  mdetralt  20921  mdetunilem2  20926  mdetunilem7  20931  mdetunilem9  20933  maducoeval2  20953  chpscmat  21154  chfacfscmulgsum  21172  chfacfpmmulgsum  21176  istopon  21224  eltg3  21274  tgidm  21292  clsval2  21362  opncldf1  21396  restbas  21470  tgrest  21471  restcld  21484  restcldr  21486  restcls  21493  restntr  21494  ordtbas2  21503  ordtbas  21504  ordtrest2lem  21515  ordtrest2  21516  pnfnei  21532  mnfnei  21533  tgcn  21564  cnconst  21596  cnindis  21604  lmss  21610  ordtt1  21691  discmp  21710  1stcrest  21765  2ndcdisj  21768  cldllycmp  21807  txbas  21879  ptpjpre1  21883  ptuni2  21888  ptbasin  21889  ptbasfi  21893  ptopn2  21896  txbasval  21918  ptpjopn  21924  ptclsg  21927  dfac14lem  21929  xkoccn  21931  ptcnp  21934  upxp  21935  ptrescn  21951  txkgen  21964  xkoptsub  21966  xkopt  21967  xkoco1cn  21969  xkoco2cn  21970  xkococn  21972  xkoinjcn  21999  ordthmeolem  22113  ptuncnv  22119  nrmhaus  22138  fbssint  22150  fbfinnfr  22153  fbasrn  22196  isufil2  22220  filufint  22232  rnelfm  22265  fmfnfmlem2  22267  fmfnfmlem3  22268  fmfnfmlem4  22269  fmfnfm  22270  flimtopon  22282  flimclslem  22296  fclstopon  22324  fclscf  22337  flimfnfcls  22340  alexsublem  22356  alexsubALTlem3  22361  alexsubALTlem4  22362  ptcmplem2  22365  tmdgsum2  22408  symgtgp  22413  cldsubg  22422  qustgplem  22432  tgptsmscld  22462  tsmsxplem1  22464  imasdsf1olem  22686  blssps  22737  blss  22738  stdbdxmet  22828  methaus  22833  metrest  22837  nrginvrcn  23004  nmoeq0  23048  blssioo  23106  xrtgioo  23117  xrsxmet  23120  reconnlem1  23137  reconnlem2  23138  xrge0tsms  23145  elcncf1di  23206  iccpnfcnv  23251  evth  23266  lebnumlem1  23268  lebnumlem2  23269  lebnumlem3  23270  nmoleub3  23426  minveclem3b  23734  ivthlem2  23756  ivthlem3  23757  elovolm  23779  ovolmge0  23781  ovoliun  23809  ovolicc2lem3  23823  ovolicc2  23826  voliunlem3  23856  dyaddisj  23900  dyadmax  23902  opnmblALT  23907  ismbfd  23943  ismbf2d  23944  mbfimaopnlem  23959  mbfimaopn2  23961  i1fmullem  23998  i1fres  24009  itg1climres  24018  mbfi1fseqlem4  24022  itg2lcl  24031  itgsplitioo  24141  ellimc2  24178  rolle  24290  dvlip  24293  dvge0  24306  dvne0  24311  lhop1lem  24313  tdeglem4  24357  degltlem1  24369  deg1nn0clb  24387  deg1lt0  24388  dvdsq1p  24457  ply1rem  24460  fta1g  24464  elply2  24489  plyf  24491  ne0p  24500  plyeq0lem  24503  plypf1  24505  0dgrb  24539  coe1termlem  24551  dgrcolem2  24567  plymul0or  24573  plyrem  24597  fta1  24600  quotcan  24601  aalioulem3  24626  eff1olem  24833  lognegb  24874  eflogeq  24886  argregt0  24894  argrege0  24895  tanarg  24903  cxpexp  24952  cxpeq0  24962  mulcxp  24969  cxpeq  25039  atans2  25210  scvxcvx  25265  dmgmaddn0  25302  isppw2  25394  vmappw  25395  vmacl  25397  efvmacl  25399  isnsqf  25414  mumullem2  25459  sqff1o  25461  dvdsppwf1o  25465  ppiublem1  25480  vmalelog  25483  chtublem  25489  fsumvma  25491  perfectlem2  25508  perfect  25509  bposlem1  25562  lgsmod  25601  lgsne0  25613  lgsdirnn0  25622  lgsqr  25629  lgsdchr  25633  gausslemma2dlem1a  25643  gausslemma2dlem6  25650  lgseisenlem2  25654  lgsquadlem1  25658  lgsquadlem2  25659  2lgslem1b  25670  2sqlem2  25696  mul2sq  25697  2sqlem7  25702  dchrisum0fno1  25789  pntrsumbnd2  25845  ostthlem1  25905  ostth2lem2  25912  ostth3  25916  ostth  25917  colinearalg  26399  axpasch  26430  axlowdimlem16  26446  axlowdimlem17  26447  axlowdim  26450  axcontlem2  26454  axcontlem4  26456  axcontlem7  26459  lpvtx  26556  edglnl  26631  numedglnl  26632  usgredgop  26658  usgrexmplef  26744  uhgrspansubgrlem  26775  uhgrspan1  26788  nbusgredgeu0  26853  nb3grprlem2  26866  cusgrsize2inds  26938  vtxd0nedgb  26973  rusgrpropnb  27068  upgrwlkvtxedg  27129  wlkp1lem1  27161  wlkp1lem6  27166  wlkp1lem8  27168  usgr2wlkneq  27245  crctcshwlk  27308  crctcsh  27310  iswwlksnon  27339  wlkiswwlks1  27353  wwlksnextbi  27382  wwlksnextbiOLD  27383  wwlksnextproplem2  27411  wwlksnextproplem2OLD  27412  wspthsnonn0vne  27423  clwlkclwwlklem2  27506  clwwisshclwws  27530  erclwwlktr  27537  clwwlkext2edg  27579  erclwwlkntr  27595  clwlknf1oclwwlknlem2  27607  clwlknf1oclwwlknlem3  27608  clwlknf1oclwwlkn  27609  clwlknf1oclwwlknlem3OLD  27610  clwlknf1oclwwlknOLD  27611  clwwlknonccat  27624  0wlkons1  27650  3wlkdlem6  27694  eupth2eucrct  27747  frgrwopreglem2  27847  2clwwlk2clwwlk  27887  2clwwlk2clwwlkOLD  27888  wlkl0  27920  nvmul0or  28204  ipasslem5  28389  ipasslem11  28394  hvmul0or  28581  his6  28655  hhssnv  28820  ocsh  28841  ocin  28854  shsidmi  28942  chnlen0  29002  h1de2bi  29112  h1de2ctlem  29113  h1de2ci  29114  spansni  29115  3oalem1  29220  nmcexi  29584  atcveq0  29906  chcv1  29913  cdjreui  29990  cdj3lem2b  29995  xrge0tsmsd  30527  ccfldextdgrr  30683  ordtrest2NEWlem  30806  ordtrest2NEW  30807  xrge0iifcnv  30817  esumc  30951  esumpcvgval  30978  ballotlemfc0  31393  ballotlemfcc  31394  subfacp1lem4  32012  subfacp1lem5  32013  erdszelem8  32027  sconnpi1  32068  cvmsss2  32103  cvmlift2lem12  32143  satf00  32181  sat1el2xp  32186  fmla0xp  32190  msubco  32295  msubvrs  32324  sinccvglem  32432  untsucf  32453  dfpo2  32508  eqfunresadj  32521  dfrdg2  32558  trpred0  32593  frrlem12  32652  frrlem13  32653  nolesgn2ores  32697  nolt02o  32717  nosupbnd2  32734  noetalem3  32737  colineardim1  33040  btwnconn1lem14  33079  segleantisym  33094  colinbtwnle  33097  outsidele  33111  lineunray  33126  linethru  33132  elicc3  33183  opnregcld  33196  cldregopn  33197  fnejoin2  33235  dissneqlem  34060  icorempo  34071  relowlssretop  34083  relowlpssretop  34084  rdgssun  34098  finxpsuclem  34116  lindsenlbs  34325  ptrecube  34330  poimirlem6  34336  poimirlem7  34337  poimirlem16  34346  poimirlem17  34347  poimirlem19  34349  poimirlem20  34350  poimirlem21  34351  poimirlem22  34352  poimirlem23  34353  poimirlem24  34354  poimirlem25  34355  poimirlem26  34356  poimirlem27  34357  poimirlem29  34359  poimirlem30  34360  poimirlem31  34361  poimirlem32  34362  itg2addnclem3  34383  ftc1anclem6  34410  dvasin  34416  unirep  34427  sdclem2  34456  ssbnd  34505  prdsbnd  34510  cntotbnd  34513  heibor1lem  34526  rrnequiv  34552  ismndo2  34591  grpoeqdivid  34598  isdrngo3  34676  crngohomfo  34723  0idl  34742  1idl  34743  divrngidl  34745  smprngopr  34769  prnc  34784  ispridlc  34787  riotaclbgBAD  35532  lshpdisj  35565  lsateln0  35573  lsatcveq0  35610  opnlen0  35766  cmtbr4N  35833  cvrnbtwn2  35853  cvrnbtwn4  35857  atcvreq0  35892  cvlatexch1  35914  exatleN  35982  atlelt  36016  ps-2  36056  llnn0  36094  lplnn0N  36125  islpln2a  36126  lvoln0N  36169  islvol2aN  36170  4at  36191  dalemcea  36238  dalem3  36242  pmapglb2N  36349  pmapglb2xN  36350  cdlema1N  36369  cdlemb  36372  paddasslem17  36414  llnexchb2lem  36446  llnexchb2  36447  lhpat3  36624  ltrnid  36713  trlne  36763  cdlemc4  36772  cdleme11h  36844  cdlemednuN  36878  cdlemg1a  37148  tendoeq2  37352  tendoid0  37403  dva1dim  37563  dib1dim  37743  dihlatat  37915  dochkrshp4  37967  dochkr1  38056  lclkrlem2e  38089  lcfrlem16  38136  lcfrlem28  38148  mapd0  38243  hdmap14lem13  38458  fnsnbt  38562  frlmsnic  38583  reladdrsub  38645  elrfi  38683  mrefg2  38696  eldiophb  38746  eldioph2b  38752  diophin  38762  diophun  38763  rexzrexnn0  38794  eldioph4b  38801  diophren  38803  rencldnfilem  38810  pellexlem6  38824  jm2.19  38983  rmydioph  39004  expdiophlem1  39011  expdioph  39013  lnr2i  39109  lpirlnr  39110  hbtlem2  39117  hbtlem4  39119  hbtlem6  39122  dgrsub2  39128  dgraa0p  39142  rngunsnply  39166  radcnvrat  40059  pm14.24  40178  addrcom  40223  afveu  42756  dfafn5b  42764  rlimdmafv  42780  afv2eu  42841  rlimdmafv2  42861  el1fzopredsuc  42929  sprvalpw  43008  prprvalpw  43043  reupr  43050  fmtnofac2lem  43096  proththdlem  43144  perfectALTVlem2  43253  perfectALTV  43254  gbowpos  43290  gbowgt5  43293  gboge9  43295  nnsum4primesodd  43327  nnsum4primesoddALTV  43328  isomuspgr  43365  lincellss  43846  lindsrng01  43888  suppdm  43931  nnpw2pb  44013  itsclc0xyqsolr  44122