Theorem syl5ibrcom 237

Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)

Hypotheses

Ref	Expression
syl5ibr.1	|- ( ph -> th )
syl5ibr.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
syl5ibrcom	|- ( ph -> ( ch -> ps ) )

Proof of Theorem syl5ibrcom

Step	Hyp	Ref	Expression
1		syl5ibr.1	. . 3 |- ( ph -> th )
2		syl5ibr.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	1, 2	syl5ibr 236	. 2 |- ( ch -> ( ph -> ps ) )
4	3	com12 32	1 |- ( ph -> ( ch -> ps ) )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  biimprcd  240  elsn2g  4210  preq1b  4377  elpreqprb  4397  reusv2lem2OLD  4870  reusv3  4876  alxfr  4878  reuhypd  4895  opth1  4944  euotd  4975  otiunsndisj  4980  tz7.2  5098  frsn  5189  elsnxp  5677  ordtri1  5756  ordtri3  5759  fvmptdv2  6298  fveqressseq  6355  foco2  6379  foco2OLD  6380  fsn  6402  fnsnb  6432  fmptsng  6434  fmptsnd  6435  fconst2g  6468  fnprb  6472  fntpb  6473  funfvima  6492  soisoi  6578  isores3  6585  riotaeqimp  6634  eusvobj2  6643  ovmpt2dv2  6794  f1opw2  6888  sorpssun  6944  sorpssin  6945  oneqmin  7005  nlimsucg  7042  onzsl  7046  tfinds  7059  funcnvuni  7119  opiota  7229  mpt2sn  7268  suppssov1  7327  suppssfv  7331  brtpos  7361  wfrlem10  7424  wfrlem14  7428  wfrlem15  7429  seqomlem1  7545  seqomlem2  7546  omordi  7646  omord  7648  omwordi  7651  oeeui  7682  nnmordi  7711  nnmord  7712  nnmwordi  7715  nnawordex  7717  nnaordex  7718  nneob  7732  omsmolem  7733  qsss  7808  eroveu  7842  mapsncnv  7904  ralxpmap  7907  elixpsn  7947  ixpsnf1o  7948  boxcutc  7951  pw2f1olem  8064  2pwne  8116  mapxpen  8126  mapunen  8129  php  8144  unxpdomlem2  8165  en1eqsnbi  8191  isfiniteg  8220  fofinf1o  8241  f1opwfi  8270  elfiun  8336  oieu  8444  brwdom2  8478  wdomtr  8480  ixpiunwdom  8496  en3lplem1  8511  suc11reg  8516  inf3lemd  8524  cantnfvalf  8562  cantnflt  8569  cantnfp1lem3  8577  cantnflem2  8587  r1tr  8639  dfac8alem  8852  wdomnumr  8887  isinfcard  8915  aceq3lem  8943  dfac5lem4  8949  dfac5  8951  dfac2  8953  coftr  9095  fin23lem28  9162  fin23lem29  9163  fin1a2lem11  9232  fin1a2lem12  9233  fin1a2lem13  9234  hsmexlem9  9247  axdclem  9341  pwcfsdom  9405  gchdomtri  9451  fpwwe2  9465  gchpwdom  9492  gchhar  9501  addnidpi  9723  nqereu  9751  genpv  9821  genpdm  9824  distrlem5pr  9849  mulid1  10037  ltne  10134  mul02  10214  cnegex  10217  mul0or  10667  negfi  10971  sup2  10979  supaddc  10990  supadd  10991  supmul1  10992  supmul  10995  creur  11014  creui  11015  cju  11016  nnsub  11059  un0addcl  11326  un0mulcl  11327  nn0sub  11343  elz2  11394  zaddcl  11417  suprzcl2  11778  qmulz  11791  qre  11793  qnegcl  11805  xrmax1  12006  xrmin2  12009  max1ALT  12017  xlesubadd  12093  xmulass  12117  xlemul1a  12118  xrsupexmnf  12135  xrinfmexpnf  12136  xrub  12142  iccid  12220  fzsn  12383  fzsuc2  12398  fz1sbc  12416  elfzp12  12419  modmuladd  12712  seqid3  12845  bcval5  13105  bcpasc  13108  hashbnd  13123  hashnnn0genn0  13131  hashprg  13182  hashprgOLD  13183  hashfzo  13216  wrdl1s1  13394  cats1un  13475  shftlem  13808  replim  13856  absmod0  14043  absz  14051  rlimdm  14282  summolem2  14447  summo  14448  zsum  14449  fsum  14451  fsummulc2  14516  fsumconst  14522  fsum00  14530  incexclem  14568  isumsplit  14572  infcvgaux1i  14589  prodmolem2  14665  prodmo  14666  zprod  14667  fprod  14671  prodsn  14692  prodsnf  14694  fprodconst  14708  ruclem2  14961  fzo0dvdseq  15045  bitsf1ocnv  15166  sadcaddlem  15179  smueqlem  15212  gcdabs1  15251  bezoutlem1  15256  bezoutlem3  15258  bezoutlem4  15259  dvdsgcd  15261  dvdsmulgcd  15274  lcmgcdeq  15325  lcmf  15346  lcmfunsnlem1  15350  lcmfunsnlem2lem2  15352  isprm2lem  15394  dvdsprime  15400  isprm5  15419  coprm  15423  prmdvdsexpr  15429  rpexp  15432  phibndlem  15475  dfphi2  15479  hashgcdlem  15493  odzdvds  15500  nnoddn2prm  15516  pythagtriplem1  15521  iserodd  15540  pceulem  15550  pcqmul  15558  pcqcl  15561  pcxcl  15565  pcneg  15578  pcabs  15579  pcgcd1  15581  pcz  15585  pcprmpw2  15586  pcprmpw  15587  dvdsprmpweqle  15590  difsqpwdvds  15591  pcaddlem  15592  pcadd  15593  pcmpt  15596  pockthg  15610  prmreclem5  15624  4sqlem4  15656  mul4sq  15658  vdwapun  15678  vdwlem2  15686  vdwlem6  15690  vdwlem8  15692  vdwlem13  15697  0ram  15724  ram0  15726  ramcl  15733  cshwsiun  15806  wunress  15940  firest  16093  xpscfv  16222  isssc  16480  pospo  16973  latnlej  17068  gsumval2a  17279  mnd1id  17332  mulgnn0p1  17552  mulgnn0ass  17578  gicsubgen  17721  symg1bas  17816  psgnunilem1  17913  psgnunilem2  17915  mndodcongi  17962  oddvdsnn0  17963  odnncl  17964  oddvds  17966  odeq  17969  odeq1  17977  pgpfi2  18021  sylow2a  18034  sylow2blem3  18037  sylow3lem6  18047  lsmelvalm  18066  lsmsubm  18068  lsmsubg  18069  lsmmod  18088  lsmdisj2  18095  efgmnvl  18127  efgtlen  18139  efgs1b  18149  efgrelexlemb  18163  efgredeu  18165  efgcpbllemb  18168  frgpuptinv  18184  frgpup3lem  18190  qusabl  18268  frgpnabllem1  18276  cyggeninv  18285  cyggenod  18286  cygabl  18292  gsumval3eu  18305  dprdssv  18415  dprdfeq0  18421  dprdsubg  18423  dprddisj2  18438  ablfacrp  18465  pgpfac1lem3  18476  pgpfaclem2  18481  dvreq1  18693  irredn1  18706  drngmul0or  18768  isabvd  18820  abvdom  18838  issrngd  18861  lmodfopnelem2  18900  lss1d  18963  lspsneq0  19012  lbspss  19082  lsmcl  19083  lvecvs0or  19108  lspindpi  19132  lidl1el  19218  lpiss  19250  lidldvgen  19255  nzrunit  19267  rrgeq0  19290  domneq0  19297  mplsubrglem  19439  mplmonmul  19464  mplcoe5lem  19467  coe1tmmul2  19646  coe1tmmul  19647  pf1ind  19719  qsssubdrg  19805  zringlpirlem1  19832  znfld  19909  znunit  19912  znrrg  19914  cygznlem3  19918  frgpcyg  19922  psgnghm  19926  ipeq0  19983  cssincl  20032  lsmcss  20036  obselocv  20072  dsmmacl  20085  dsmmlss  20088  mat1dimelbas  20277  mdetralt  20414  mdetunilem2  20419  mdetunilem7  20424  mdetunilem9  20426  maducoeval2  20446  chpscmat  20647  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  istopon  20717  eltg3  20766  tgidm  20784  clsval2  20854  opncldf1  20888  restbas  20962  tgrest  20963  restcld  20976  restcldr  20978  restcls  20985  restntr  20986  ordtbas2  20995  ordtbas  20996  ordtrest2lem  21007  ordtrest2  21008  pnfnei  21024  mnfnei  21025  tgcn  21056  cnconst  21088  cnindis  21096  lmss  21102  ordtt1  21183  discmp  21201  1stcrest  21256  2ndcdisj  21259  cldllycmp  21298  txbas  21370  ptpjpre1  21374  ptuni2  21379  ptbasin  21380  ptbasfi  21384  ptopn2  21387  txbasval  21409  ptpjopn  21415  ptclsg  21418  dfac14lem  21420  xkoccn  21422  ptcnp  21425  upxp  21426  ptrescn  21442  txkgen  21455  xkoptsub  21457  xkopt  21458  xkoco1cn  21460  xkoco2cn  21461  xkococn  21463  xkoinjcn  21490  ordthmeolem  21604  ptuncnv  21610  nrmhaus  21629  fbssint  21642  fbfinnfr  21645  fbasrn  21688  isufil2  21712  filufint  21724  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem3  21760  fmfnfmlem4  21761  fmfnfm  21762  flimtopon  21774  flimclslem  21788  fclstopon  21816  fclscf  21829  flimfnfcls  21832  alexsublem  21848  alexsubALTlem3  21853  alexsubALTlem4  21854  ptcmplem2  21857  tmdgsum2  21900  symgtgp  21905  cldsubg  21914  qustgplem  21924  tgptsmscld  21954  tsmsxplem1  21956  imasdsf1olem  22178  blssps  22229  blss  22230  stdbdxmet  22320  methaus  22325  metrest  22329  nrginvrcn  22496  nmoeq0  22540  blssioo  22598  xrtgioo  22609  xrsxmet  22612  reconnlem1  22629  reconnlem2  22630  xrge0tsms  22637  elcncf1di  22698  iccpnfcnv  22743  evth  22758  lebnumlem1  22760  lebnumlem2  22761  lebnumlem3  22762  nmoleub3  22919  minveclem3b  23199  ivthlem2  23221  ivthlem3  23222  elovolm  23243  ovolmge0  23245  ovoliun  23273  ovolicc2lem3  23287  ovolicc2  23290  voliunlem3  23320  dyaddisj  23364  dyadmax  23366  opnmblALT  23371  ismbfd  23407  ismbf2d  23408  mbfimaopnlem  23422  mbfimaopn2  23424  i1fmullem  23461  i1fres  23472  itg1climres  23481  mbfi1fseqlem4  23485  itg2lcl  23494  itgsplitioo  23604  ellimc2  23641  rolle  23753  dvlip  23756  dvge0  23769  dvne0  23774  lhop1lem  23776  tdeglem4  23820  degltlem1  23832  deg1nn0clb  23850  deg1lt0  23851  dvdsq1p  23920  ply1rem  23923  fta1g  23927  elply2  23952  plyf  23954  ne0p  23963  plyeq0lem  23966  plypf1  23968  0dgrb  24002  coe1termlem  24014  dgrcolem2  24030  plymul0or  24036  plyrem  24060  fta1  24063  quotcan  24064  aalioulem3  24089  eff1olem  24294  lognegb  24336  eflogeq  24348  argregt0  24356  argrege0  24357  tanarg  24365  cxpexp  24414  cxpeq0  24424  mulcxp  24431  cxpeq  24498  atans2  24658  scvxcvx  24712  dmgmaddn0  24749  isppw2  24841  vmappw  24842  vmacl  24844  efvmacl  24846  isnsqf  24861  mumullem2  24906  sqff1o  24908  dvdsppwf1o  24912  ppiublem1  24927  vmalelog  24930  chtublem  24936  fsumvma  24938  perfectlem2  24955  perfect  24956  bposlem1  25009  lgsmod  25048  lgsne0  25060  lgsdirnn0  25069  lgsqr  25076  lgsdchr  25080  gausslemma2dlem1a  25090  gausslemma2dlem6  25097  lgseisenlem2  25101  lgsquadlem1  25105  lgsquadlem2  25106  2lgslem1b  25117  2sqlem2  25143  mul2sq  25144  2sqlem7  25149  dchrisum0fno1  25200  pntrsumbnd2  25256  ostthlem1  25316  ostth2lem2  25323  ostth3  25327  ostth  25328  colinearalg  25790  axpasch  25821  axlowdimlem16  25837  axlowdimlem17  25838  axlowdim  25841  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  lpvtx  25963  edglnl  26038  numedglnl  26039  usgredgop  26065  usgrexmplef  26151  uhgrspansubgrlem  26182  uhgrspan1  26195  nbusgredgeu0  26270  nb3grprlem2  26283  cusgrsize2inds  26349  vtxd0nedgb  26384  rusgrpropnb  26479  upgrwlkvtxedg  26541  wlkp1lem1  26570  wlkp1lem6  26575  wlkp1lem8  26577  usgr2wlkneq  26652  crctcshwlk  26714  crctcsh  26716  wlkiswwlks1  26753  wlkwwlksur  26783  wwlksnextbi  26789  wwlksnextproplem2  26805  wspthsnonn0vne  26813  clwlkclwwlklem2  26901  clwwlksext2edg  26923  clwwisshclwws  26928  erclwwlkstr  26936  erclwwlksntr  26948  clwlksfclwwlk1hash  26960  0wlkons1  26982  3wlkdlem6  27025  eupth2eucrct  27077  frgrwopreglem2  27177  nvmul0or  27505  ipasslem5  27690  ipasslem11  27695  hvmul0or  27882  his6  27956  hhssnv  28121  ocsh  28142  ocin  28155  shsidmi  28243  chnlen0  28303  h1de2bi  28413  h1de2ctlem  28414  h1de2ci  28415  spansni  28416  3oalem1  28521  nmcexi  28885  atcveq0  29207  chcv1  29214  cdjreui  29291  cdj3lem2b  29296  xrge0tsmsd  29785  ordtrest2NEWlem  29968  ordtrest2NEW  29969  xrge0iifcnv  29979  esumc  30113  esumpcvgval  30140  ballotlemfc0  30554  ballotlemfcc  30555  bnj145OLD  30795  subfacp1lem4  31165  subfacp1lem5  31166  erdszelem8  31180  sconnpi1  31221  cvmsss2  31256  cvmlift2lem12  31296  msubco  31428  msubvrs  31457  sinccvglem  31566  untsucf  31587  dfpo2  31645  eqfunresadj  31659  dfrdg2  31701  trpred0  31736  frrlem4  31783  nolesgn2ores  31825  nolt02o  31845  nosupbnd2  31862  noetalem3  31865  colineardim1  32168  btwnconn1lem14  32207  segleantisym  32222  colinbtwnle  32225  outsidele  32239  lineunray  32254  linethru  32260  elicc3  32311  opnregcld  32325  cldregopn  32326  fnejoin2  32364  dissneqlem  33187  icorempt2  33199  relowlssretop  33211  relowlpssretop  33212  finxpsuclem  33234  lindsenlbs  33404  ptrecube  33409  poimirlem6  33415  poimirlem7  33416  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  itg2addnclem3  33463  ftc1anclem6  33490  dvasin  33496  unirep  33507  sdclem2  33538  ssbnd  33587  prdsbnd  33592  cntotbnd  33595  heibor1lem  33608  rrnequiv  33634  ismndo2  33673  grpoeqdivid  33680  isdrngo3  33758  crngohomfo  33805  0idl  33824  1idl  33825  divrngidl  33827  smprngopr  33851  prnc  33866  ispridlc  33869  riotaclbgBAD  34240  lshpdisj  34274  lsateln0  34282  lsatcveq0  34319  opnlen0  34475  cmtbr4N  34542  cvrnbtwn2  34562  cvrnbtwn4  34566  atcvreq0  34601  cvlatexch1  34623  exatleN  34690  atlelt  34724  ps-2  34764  llnn0  34802  lplnn0N  34833  islpln2a  34834  lvoln0N  34877  islvol2aN  34878  4at  34899  dalemcea  34946  dalem3  34950  pmapglb2N  35057  pmapglb2xN  35058  cdlema1N  35077  cdlemb  35080  paddasslem17  35122  llnexchb2lem  35154  llnexchb2  35155  lhpat3  35332  ltrnid  35421  trlne  35472  cdlemc4  35481  cdleme11h  35553  cdlemednuN  35587  cdlemg1a  35858  tendoeq2  36062  tendoid0  36113  dva1dim  36273  dib1dim  36454  dihlatat  36626  dochkrshp4  36678  dochkr1  36767  lclkrlem2e  36800  lcfrlem16  36847  lcfrlem28  36859  mapd0  36954  hdmap14lem13  37172  elrfi  37257  mrefg2  37270  eldiophb  37320  eldioph2b  37326  diophin  37336  diophun  37337  rexzrexnn0  37368  eldioph4b  37375  diophren  37377  rencldnfilem  37384  pellexlem6  37398  jm2.19  37560  rmydioph  37581  expdiophlem1  37588  expdioph  37590  lnr2i  37686  lpirlnr  37687  hbtlem2  37694  hbtlem4  37696  hbtlem6  37699  dgrsub2  37705  dgraa0p  37719  rngunsnply  37743  radcnvrat  38513  pm14.24  38633  addrcom  38679  afveu  41233  dfafn5b  41241  rlimdmafv  41257  el1fzopredsuc  41335  fmtnofac2lem  41480  proththdlem  41530  perfectALTVlem2  41631  perfectALTV  41632  gbowpos  41647  gbowgt5  41650  gboge9  41652  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  sprvalpw  41730  lincellss  42215  lindsrng01  42257  suppdm  42300  nnpw2pb  42381