Theorem syl6bi 162

Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)

Hypotheses

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

Assertion

Ref	Expression
syl6bi	|- ( ph -> ( ps -> th ) )

Proof of Theorem syl6bi

Step	Hyp	Ref	Expression
1		syl6bi.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	biimpd 143	. 2 |- ( ph -> ( ps -> ch ) )
3		syl6bi.2	. 2 |- ( ch -> th )
4	2, 3	syl6 33	1 |- ( ph -> ( ps -> th ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.33bdc  1623  ax11i  1707  equveli  1752  eupickbi  2101  nfabdw  2331  rgen2a  2524  reu6  2919  sseq0  3456  disjel  3469  preq12b  3757  prel12  3758  prneimg  3761  elinti  3840  exmidundif  4192  opthreg  4540  elreldm  4837  issref  4993  relcnvtr  5130  relresfld  5140  funopg  5232  funimass2  5276  f0dom0  5391  fvimacnv  5611  elunirn  5745  oprabid  5885  op1steq  6158  f1o2ndf1  6207  reldmtpos  6232  rntpos  6236  nntri3or  6472  nnaordex  6507  nnawordex  6508  findcard2  6867  findcard2s  6868  mkvprop  7134  cc2lem  7228  lt2addnq  7366  lt2mulnq  7367  genpelvl  7474  genpelvu  7475  distrlem5prl  7548  distrlem5pru  7549  caucvgprlemnkj  7628  map2psrprg  7767  rereceu  7851  ltxrlt  7985  0mnnnnn0  9167  elnnnn0b  9179  nn0le2is012  9294  btwnz  9331  uz11  9509  nn01to3  9576  zq  9585  xrltso  9753  xltnegi  9792  xnn0lenn0nn0  9822  xnn0xadd0  9824  iccleub  9888  fzdcel  9996  uznfz  10059  2ffzeq  10097  elfzonlteqm1  10166  icogelb  10222  flqeqceilz  10274  modqadd1  10317  modqmul1  10333  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  fzfig  10386  m1expeven  10523  qsqeqor  10586  caucvgrelemcau  10944  rexico  11185  fisumss  11355  fsum2dlemstep  11397  ntrivcvgap  11511  fprodssdc  11553  fprod2dlemstep  11585  0dvds  11773  alzdvds  11814  opoe  11854  omoe  11855  opeo  11856  omeo  11857  m1exp1  11860  nn0enne  11861  nn0o1gt2  11864  gcdneg  11937  dfgcd2  11969  algcvgblem  12003  algcvga  12005  eucalglt  12011  coprmdvds  12046  divgcdcoprmex  12056  cncongr1  12057  prm2orodd  12080  prm23lt5  12217  pockthi  12310  ismnddef  12654  tg2  12854  tgcl  12858  neii1  12941  neii2  12943  txlm  13073  reopnap  13332  tgioo  13340  addcncntoplem  13345  bj-elssuniab  13826  bj-nn0sucALT  14013  triap  14061