Theorem syl5bi 151

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem syl5bi

Step	Hyp	Ref	Expression
1		syl5bi.1	. . 3 |- ( ph <-> ps )
2	1	biimpi 119	. 2 |- ( ph -> ps )
3		syl5bi.2	. 2 |- ( ch -> ( ps -> th ) )
4	2, 3	syl5 32	1 |- ( ch -> ( ph -> 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:  3imtr4g  204  ancomsd  267  pm2.13dc  875  3jao  1291  19.33b2  1617  sbequ2  1757  sbi1v  1879  mor  2056  2euex  2101  eqneqall  2345  necon3ad  2377  necon1aidc  2386  necon4addc  2405  elnelall  2442  spcimgft  2801  spcimegft  2803  rspc  2823  rspcimdv  2830  rspc2gv  2841  euind  2912  2reuswapdc  2929  reuind  2930  sbciegft  2980  rspsbc  3032  preqr2g  3746  prel12  3750  intss1  3838  intmin  3843  iinss  3916  disjiun  3976  trel3  4087  trin  4089  repizf2  4140  exmidsssnc  4181  copsexg  4221  po3nr  4287  sowlin  4297  eusvnfb  4431  reusv3  4437  ssorduni  4463  ordsucim  4476  tfis2f  4560  ssrelrel  4703  relop  4753  iss  4929  poirr2  4995  funopg  5221  funssres  5229  funun  5231  funcnvuni  5256  fv3  5508  fvmptt  5576  dff4im  5630  f1eqcocnv  5758  oprabid  5870  f1o2ndf1  6192  poxp  6196  reldmtpos  6217  rntpos  6221  smoiun  6265  tfrlem1  6272  tfrlemi1  6296  tfrexlem  6298  tfri3  6331  nntri3or  6457  qsss  6556  th3qlem1  6599  ixpsnf1o  6698  phplem4  6817  fimax2gtri  6863  fiintim  6890  fisseneq  6893  sbthlemi10  6927  supmoti  6954  suplub2ti  6962  ordiso2  6996  ltmpig  7276  prcdnql  7421  prcunqu  7422  recexprlem1ssl  7570  recexprlem1ssu  7571  recexprlemss1l  7572  recexprlemss1u  7573  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  caucvgprlemladdrl  7615  mulgt0sr  7715  suplocsrlem  7745  axprecex  7817  ltxrlt  7960  addid0  8267  negf1o  8276  cju  8852  nngt1ne1  8888  nnsub  8892  0mnnnnn0  9142  un0addcl  9143  un0mulcl  9144  zapne  9261  eluzuzle  9470  indstr  9527  elpq  9582  xposdif  9814  ixxdisj  9835  icodisj  9924  uzsubsubfz  9978  elfzmlbp  10063  fzofzim  10119  subfzo0  10173  addmodlteq  10329  seq3f1olemp  10433  expcl2lemap  10463  expnegzap  10485  expaddzap  10495  expmulzap  10497  facwordi  10649  bccl  10676  hashfacen  10745  ovshftex  10757  cau3lem  11052  maxabslemval  11146  rexanre  11158  xrmaxiflemval  11187  2clim  11238  summodc  11320  fsum2dlemstep  11371  fsumiun  11414  prodmodc  11515  fprod2dlemstep  11559  odd2np1lem  11805  oddge22np1  11814  sqoddm1div8z  11819  divalglemeunn  11854  divalglemeuneg  11856  gcd0id  11908  divgcdcoprm0  12029  prmdvdsexpr  12078  prmfac1  12080  qnumdencl  12115  hashdvds  12149  prm23lt5  12191  pcneg  12252  prmpwdvds  12281  ctinf  12359  tgcl  12664  epttop  12690  txbas  12858  txbasval  12867  txcnp  12871  txdis1cn  12878  bldisj  13001  reopnap  13138  dvfgg  13257  lgsdir2lem2  13530  bj-vtoclgft  13616  bj-charfun  13649  bj-charfunbi  13653  bj-indind  13774  bj-nntrans  13793  bj-nnelirr  13795  triap  13868