Theorem syl5ibcom 155

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

Hypotheses

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

Assertion

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

Proof of Theorem syl5ibcom

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimpcd  159  mob2  2960  rmob  3099  preqr1g  3820  issod  4384  sotritrieq  4390  nsuceq0g  4483  suctr  4486  nordeq  4610  suc11g  4623  iss  5024  poirr2  5094  xp11m  5140  tz6.12c  5629  fnbrfvb  5642  fvelimab  5658  foeqcnvco  5882  f1eqcocnv  5883  acexmidlemcase  5962  nna0r  6587  nnawordex  6638  ectocld  6711  ecoptocl  6732  mapsn  6800  eqeng  6880  fopwdom  6958  ordiso  7164  ltexnqq  7556  nsmallnqq  7560  nqprloc  7693  aptiprleml  7787  map2psrprg  7953  0re  8107  lttri3  8187  0cnALT  8297  reapti  8687  recnz  9501  zneo  9509  uzn0  9699  flqidz  10466  ceilqidz  10498  modqid2  10533  modqmuladdnn0  10550  frec2uzrand  10587  frecuzrdgtcl  10594  seq3id  10707  seq3z  10710  facdiv  10920  facwordi  10922  wrdnval  11061  wrdl1s1  11122  maxleb  11642  fsumf1o  11816  dvdsnegb  12234  odd2np1lem  12298  odd2np1  12299  ltoddhalfle  12319  halfleoddlt  12320  opoe  12321  omoe  12322  opeo  12323  omeo  12324  gcddiv  12455  gcdzeq  12458  dvdssqim  12460  lcmgcdeq  12520  coprmdvds2  12530  rpmul  12535  divgcdcoprmex  12539  cncongr2  12541  dvdsprm  12574  coprm  12581  prmdvdsexp  12585  prmdiv  12672  pythagtriplem19  12720  pc2dvds  12768  pcadd  12778  prmpwdvds  12793  exmidunben  12912  intopsn  13314  ismgmid  13324  imasmnd2  13399  isgrpid2  13487  isgrpinv  13501  dfgrp3mlem  13545  imasgrp2  13561  imasrng  13833  imasring  13941  dvdsrcl2  13976  dvdsrtr  13978  dvdsrmul1  13979  lspsneq0  14303  dvdsrzring  14480  znunit  14536  baspartn  14637  bastop  14662  isopn3  14712  lgsdir  15627  lgsne0  15630  lgsquadlem3  15671  uhgrm  15789  upgrfnen  15809  umgrfnen  15819  bj-peano4  16090  sbthomlem  16166