Theorem syl5ib 219

Description: A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem syl5ib

Step	Hyp	Ref	Expression
1		syl5ib.1	. 2 |- ( ph -> ps )
2		syl5ib.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	2	biimpd 207	. 2 |- ( ch -> ( ps -> th ) )
4	1, 3	syl5 32	1 |- ( ch -> ( ph -> th ) )

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

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 185

This theorem is referenced by:  syl5ibcom  220  syl5ibr  221  dvelimdf  2027  sb4  2047  sbft  2070  ax12indalem  2246  ax12inda2ALT  2247  gencl  3023  spsbc  3220  eqsbc3r  3269  ssnelpss  3763  uniintsn  4186  prex  4555  copsexg  4597  ordtri3  4776  posn  4928  optocl  4934  funimass1  5512  f1ocnvb  5675  eqfnfv2  5819  elpreima  5844  fconst5  5956  dff13  5992  f1ocnvfv  6006  f1ocnvfvb  6007  fliftfun  6026  eusvobj2  6105  sorpsscmpl  6392  ssonprc  6424  xpexr  6539  xpexcnv  6541  relcnvexb  6547  dmfex  6556  frxp  6703  mpt2xopn0yelv  6751  rntpos  6779  oawordeulem  7014  oalimcl  7020  odi  7039  omeulem2  7043  oeeulem  7061  erexb  7147  unxpdomlem2  7539  dif1enOLD  7565  dif1en  7566  enp1ilem  7567  findcard2  7573  isfinite2  7591  unfi  7600  fodomfib  7612  inf0  7848  rankxplim2  8108  scott0  8114  ficardom  8152  cardaleph  8280  dfac5  8319  cflim2  8453  fin23lem23  8516  fin23lem28  8530  isf32lem5  8547  domtriomlem  8632  ac6num  8669  zorn2lem5  8690  zorn2lem6  8691  iunfo  8724  axrepndlem2  8778  axregnd  8791  axregndOLD  8792  hargch  8861  addcanpi  9089  mulcanpi  9090  indpi  9097  ltaddnq  9164  ltexnq  9165  prlem934  9223  ltaddpr2  9225  ltaprlem  9234  supsrlem  9299  ssxr  9465  ltxrlt  9466  addcan  9574  addcan2  9575  neg11  9681  negreb  9695  mulcand  9990  receu  10002  lemul1a  10204  cju  10339  nn1suc  10364  nnaddcl  10365  nndivtr  10384  znegclb  10703  zmulcl  10714  zeo  10748  uz11  10904  uzp1  10915  eqreznegel  10961  rpnnen1  11005  xrltne  11158  xneg11  11206  xnegdi  11232  xrsupss  11292  xrinfmss  11293  elfznelfzob  11652  modadd1  11766  modmul1  11773  om2uzlti  11794  bccmpl  12106  hashen  12139  fz1eqb  12145  hashfn  12159  hashnn0n0nn  12174  hashtpg  12207  eqwrd  12286  ccatopth  12385  ccatopth2  12386  swrdccatin2  12399  swrdccat3a  12406  cj11  12672  rennim  12749  cnpart  12750  sqrmo  12762  sqrgt0  12769  sqreulem  12868  sqreu  12869  lo1o1  13031  lo1eq  13067  rlimeq  13068  sumss  13222  cvgcmp  13300  efne0  13402  dvdseq  13601  divalglem8  13625  bitsinv1lem  13658  pcfac  13982  prmreclem3  14000  sectmon  14737  yoniso  15116  lublecllem  15179  oduposb  15327  grpinveu  15593  mulgass  15678  galcan  15843  symg1bas  15922  cayleylem2  15939  odbezout  16080  odeq1  16082  dprddomcld  16505  dvreq1  16807  unitrrg  17387  coe1tm  17748  frgpcyg  18028  obslbs  18177  tgss3  18613  uptx  19220  txindislem  19228  qtopeu  19311  hmeocnvb  19369  qtophmeo  19412  trufil  19505  ufinffr  19524  ghmcnp  19707  tgioo  20395  lmmcvg  20794  bcth3  20864  ovolunlem1a  21001  vitali  21115  ismbf  21130  ismbfcn  21131  rolle  21484  itgsubstlem  21542  vieta1lem2  21799  elqaalem3  21809  aacjcl  21815  efif1olem4  22023  lognegb  22060  logcj  22077  argimgt0  22083  logdmnrp  22108  logcnlem3  22111  logrec  22237  dcubic  22263  isppw  22474  rplogsumlem2  22756  pntpbnd1  22857  axlowdimlem16  23225  is2wlk  23486  grpoinveu  23731  grpoinvf  23749  diporthcom  24136  norm1exi  24675  shmodsi  24814  shmodi  24815  dfch2  24832  orthin  24871  chssoc  24921  spansncvi  25077  kbpj  25382  lnopunilem1  25436  cnlnssadj  25506  bra11  25534  strlem4  25680  strlem5  25681  hstrlem4  25688  hstrlem5  25689  dmdmd  25726  mdslle1i  25743  mdslle2i  25744  mdslmd1lem1  25751  atcvatlem  25811  atcvat4i  25823  mdsymlem3  25831  bcm1n  26101  xmulcand  26118  xreceu  26119  tpr2rico  26364  fprodser  27484  funpsstri  27598  sltres  27827  nofulllem1  27865  nofulllem2  27866  btwnintr  28072  idinside  28137  btwnconn1lem13  28152  wl-equsal1i  28398  dvtanlem  28467  fneval  28585  ismtybndlem  28731  grpoeqdivid  28772  0rngo  28853  expgrowth  29635  sbiota1  29714  nbgrassvwo2  30303  usgra2pth  30327  wwlkn0  30349  wlkiswwlk1  30350  wlklniswwlkn1  30359  wlklniswwlkn2  30360  el2wlkonot  30414  wwlksubclwwlk  30492  frg2wot1  30676  bnj1125  32079  bj-sb4v  32368  bj-sbftv  32376  bj-equsal1t  32426  bj-ldiv  32690  bj-bary1lem1  32696  bj-bary1  32697  lcvexchlem4  32778  lcvexchlem5  32779  opcon3b  32937  2dim  33210  ps-1  33217  paddclN  33582  ltrnnid  33876  cdleme22b  34081  dihmeetlem13N  35060  dih1dimatlem  35070  dihlspsnat  35074