Theorem syl5ib 211

Description: A mixed syllogism inference. (Contributed by NM, 5-Aug-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 199	. 2 |- ( ch -> ( ps -> th ) )
4	1, 3	syl5 30	1 |- ( ch -> ( ph -> th ) )

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

This theorem is referenced by:  syl5ibcom  212  syl5ibr  213  19.23tOLD  1834  nfsb4t  2129  ax11indalem  2247  ax11inda2ALT  2248  gencl  2944  spsbc  3133  eqsbc3r  3178  ssnelpss  3651  uniintsn  4047  prex  4366  ordtri3  4577  ssonprc  4731  posn  4905  optocl  4911  xpexr  5266  relcnvexb  5366  funimass1  5485  dmfex  5585  f1ocnvb  5647  eqfnfv2  5787  elpreima  5809  fconst5  5908  dff13  5963  f1ocnvfv  5975  f1ocnvfvb  5976  fliftfun  5993  frxp  6415  mpt2xopn0yelv  6423  rntpos  6451  sorpsscmpl  6492  eusvobj2  6541  oawordeulem  6756  oalimcl  6762  odi  6781  omeulem2  6785  oeeulem  6803  erexb  6889  unxpdomlem2  7273  dif1enOLD  7299  dif1en  7300  enp1ilem  7301  findcard2  7307  isfinite2  7324  unfi  7333  fodomfib  7345  inf0  7532  rankxplim2  7760  scott0  7766  ficardom  7804  cardaleph  7926  dfac5  7965  cflim2  8099  fin23lem23  8162  fin23lem28  8176  isf32lem5  8193  domtriomlem  8278  ac6num  8315  zorn2lem5  8336  zorn2lem6  8337  iunfo  8370  axrepndlem2  8424  axregnd  8435  hargch  8508  addcanpi  8732  mulcanpi  8733  indpi  8740  ltaddnq  8807  ltexnq  8808  prlem934  8866  ltaddpr2  8868  ltaprlem  8877  supsrlem  8942  ssxr  9101  ltxrlt  9102  addcan  9206  addcan2  9207  neg11  9308  negreb  9322  mulcand  9611  receu  9623  lemul1a  9820  cju  9952  nn1suc  9977  nnaddcl  9978  nndivtr  9997  znegclb  10270  zmulcl  10280  zeo  10311  uz11  10464  uzp1  10475  eqreznegel  10517  rpnnen1  10561  xrltne  10709  xneg11  10757  xnegdi  10783  xrsupss  10843  xrinfmss  10844  elfznelfzob  11148  modadd1  11233  modmul1  11234  om2uzlti  11245  bccmpl  11555  hashen  11586  fz1eqb  11592  hashfn  11604  hashnn0n0nn  11619  hashtpg  11646  ccatopth  11731  ccatopth2  11732  cj11  11922  rennim  11999  cnpart  12000  sqrmo  12012  sqrgt0  12019  sqreulem  12118  sqreu  12119  lo1o1  12281  lo1eq  12317  rlimeq  12318  sumss  12473  cvgcmp  12550  efne0  12653  dvdseq  12852  divalglem8  12875  bitsinv1lem  12908  pcfac  13223  prmreclem3  13241  sectmon  13958  yoniso  14337  lubid  14394  oduposb  14518  grpinveu  14794  mulgass  14875  galcan  15036  cayleylem2  15066  odbezout  15149  odeq1  15151  dvreq1  15753  unitrrg  16308  coe1tm  16620  frgpcyg  16809  obslbs  16912  tgss3  17006  uptx  17610  txindislem  17618  qtopeu  17701  hmeocnvb  17759  qtophmeo  17802  trufil  17895  ufinffr  17914  ghmcnp  18097  tgioo  18780  lmmcvg  19167  bcth3  19237  ovolunlem1a  19345  vitali  19458  ismbf  19475  ismbfcn  19476  rolle  19827  itgsubstlem  19885  vieta1lem2  20181  elqaalem3  20191  aacjcl  20197  efif1olem4  20400  lognegb  20437  logcj  20454  argimgt0  20460  logdmnrp  20485  logcnlem3  20488  logrec  20614  dcubic  20639  isppw  20850  rplogsumlem2  21132  pntpbnd1  21233  is2wlk  21518  grpoinveu  21763  grpoinvf  21781  diporthcom  22168  norm1exi  22705  shmodsi  22844  shmodi  22845  dfch2  22862  orthin  22901  chssoc  22951  spansncvi  23107  kbpj  23412  lnopunilem1  23466  cnlnssadj  23536  bra11  23564  strlem4  23710  strlem5  23711  hstrlem4  23718  hstrlem5  23719  dmdmd  23756  mdslle1i  23773  mdslle2i  23774  mdslmd1lem1  23781  atcvatlem  23841  atcvat4i  23853  mdsymlem3  23861  bcm1n  24104  xmulcand  24120  xreceu  24121  tpr2rico  24263  fprodser  25228  funpsstri  25335  sltres  25532  nofulllem1  25570  nofulllem2  25571  axlowdimlem16  25800  btwnintr  25857  idinside  25922  btwnconn1lem13  25937  fneval  26257  ismtybndlem  26405  grpoeqdivid  26446  0rngo  26527  expgrowth  27420  sbiota1  27502  xpexcnv  27526  swrdccat3a  28030  usgra2pth  28041  el2wlkonot  28066  frg2wot1  28160  bnj1125  29067  nfsb4twAUX7  29280  nfsb4tOLD7  29429  nfsb4tw2AUXOLD7  29430  lcvexchlem4  29520  lcvexchlem5  29521  opcon3b  29679  2dim  29952  ps-1  29959  paddclN  30324  ltrnnid  30618  cdleme22b  30823  dihmeetlem13N  31802  dih1dimatlem  31812  dihlspsnat  31816

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178