Theorem syl5ibrcom 156

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 155	. 2 |- ( ch -> ( ph -> ps ) )
4	3	com12 30	1 |- ( ph -> ( ch -> ps ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimprcd  159  elsn2g  3608  preqr1g  3745  opth1  4213  euotd  4231  tz7.2  4331  reusv3  4437  alxfr  4438  reuhypd  4448  ordsucim  4476  suc11g  4533  nlimsucg  4542  xpsspw  4715  funcnvuni  5256  fvmptdv2  5574  fsn  5656  fconst2g  5699  funfvima  5715  foco2  5721  isores3  5782  eusvobj2  5827  ovmpodv2  5971  ovelrn  5986  f1opw2  6043  suppssfv  6045  suppssov1  6046  nnmordi  6480  nnmord  6481  qsss  6556  eroveu  6588  th3qlem1  6599  mapsncnv  6657  elixpsn  6697  ixpsnf1o  6698  en1bg  6762  mapxpen  6810  en1eqsnbi  6910  updjud  7043  addnidpig  7273  enq0tr  7371  prcdnql  7421  prcunqu  7422  genipv  7446  genpelvl  7449  genpelvu  7450  distrlem5prl  7523  distrlem5pru  7524  aptiprlemu  7577  mulid1  7892  ltne  7979  cnegex  8072  creur  8850  creui  8851  cju  8852  nnsub  8892  un0addcl  9143  un0mulcl  9144  zaddcl  9227  elz2  9258  qmulz  9557  qre  9559  qnegcl  9570  elpqb  9583  xrltne  9745  xlesubadd  9815  iccid  9857  fzsn  9997  fzsuc2  10010  fz1sbc  10027  elfzp12  10030  modqmuladd  10297  bcval5  10672  bcpasc  10675  hashprg  10717  hashfzo  10731  shftlem  10754  replim  10797  sqrtsq  10982  absle  11027  maxabslemval  11146  negfi  11165  xrmaxiflemval  11187  summodclem2  11319  summodc  11320  zsumdc  11321  fsum3  11324  fsummulc2  11385  fsum00  11399  isumsplit  11428  prodmodclem2  11514  prodmodc  11515  zproddc  11516  fprodseq  11520  prodsnf  11529  fzo0dvdseq  11791  divalgmod  11860  gcdabs1  11918  dvdsgcd  11941  dvdsmulgcd  11954  lcmgcdeq  12011  isprm2lem  12044  dvdsprime  12050  coprm  12072  prmdvdsexpr  12078  rpexp  12081  phibndlem  12144  dfphi2  12148  hashgcdlem  12166  odzdvds  12173  nnoddn2prm  12188  pythagtriplem1  12193  pceulem  12222  pcqmul  12231  pcqcl  12234  pcxnn0cl  12238  pcxcl  12239  pcneg  12252  pcabs  12253  pcgcd1  12255  pcz  12259  pcprmpw2  12260  pcprmpw  12261  dvdsprmpweqle  12264  difsqpwdvds  12265  pcaddlem  12266  pcadd  12267  pcmpt  12269  pockthg  12283  4sqlem2  12315  4sqlem4  12318  mul4sq  12320  istopon  12611  eltg3  12657  tgidm  12674  restbasg  12768  tgrest  12769  tgcn  12808  cnconst  12834  lmss  12846  txbas  12858  txbasval  12867  upxp  12872  blssps  13027  blss  13028  metrest  13106  blssioo  13145  elcncf1di  13166  lgsmod  13527  lgsne0  13539  lgsdirnn0  13548  2sqlem2  13551  mul2sq  13552  2sqlem7  13557  bj-peano4  13797