Theorem syl5ibcom 153

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

Hypotheses

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

Assertion

Ref	Expression
syl5ibcom	|- ( ph -> ( ch -> th ) )

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		syl5ib.1	. . 3 |- ( ph -> ps )
2		syl5ib.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	1, 2	syl5ib 152	. 2 |- ( ch -> ( ph -> th ) )
4	3	com12 30	1 |- ( ph -> ( ch -> th ) )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  biimpcd  157  mob2  2772  rmob  2906  preqr1g  3558  issod  4074  sotritrieq  4080  nsuceq0g  4173  suctr  4176  nordeq  4287  suc11g  4300  iss  4674  poirr2  4737  xp11m  4779  tz6.12c  5224  fnbrfvb  5235  fvelimab  5250  foeqcnvco  5450  f1eqcocnv  5451  acexmidlemcase  5527  nna0r  6080  nnawordex  6124  ectocld  6195  ecoptocl  6216  eqeng  6269  fopwdom  6333  ordiso  6447  ltexnqq  6598  nsmallnqq  6602  nqprloc  6735  aptiprleml  6829  0re  7119  lttri3  7191  0cnALT  7298  reapti  7679  recnz  8440  zneo  8448  uzn0  8634  flqidz  9288  ceilqidz  9318  modqid2  9353  modqmuladdnn0  9370  frec2uzrand  9407  frecuzrdgfn  9414  iseqid  9467  iseqz  9469  facdiv  9665  facwordi  9667  maxleb  10102  dvdsnegb  10212  odd2np1lem  10271  odd2np1  10272  ltoddhalfle  10293  halfleoddlt  10294  opoe  10295  omoe  10296  opeo  10297  omeo  10298  gcddiv  10408  gcdzeq  10411  dvdssqim  10413  lcmgcdeq  10465  coprmdvds2  10475  rpmul  10480  divgcdcoprmex  10484  cncongr2  10486  dvdsprm  10518  coprm  10523  prmdvdsexp  10527  bj-peano4  10750