Theorem biimtrid 152

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
biimtrid.1	|- ( ph <-> ps )
biimtrid.2	|- ( ch -> ( ps -> th ) )

Assertion

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

Proof of Theorem biimtrid

Step	Hyp	Ref	Expression
1		biimtrid.1	. . 3 |- ( ph <-> ps )
2	1	biimpi 120	. 2 |- ( ph -> ps )
3		biimtrid.2	. 2 |- ( ch -> ( ps -> th ) )
4	2, 3	syl5 32	1 |- ( ch -> ( ph -> 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:  3imtr4g  205  ancomsd  269  pm2.13dc  897  3jao  1342  19.33b2  1682  sbequ2  1822  sbi1v  1946  mor  2129  2euex  2174  eqneqall  2430  necon3ad  2462  necon1aidc  2471  necon4addc  2490  elnelall  2527  spcimgft  2901  spcimegft  2903  rspc  2923  rspcimdv  2930  rspc2gv  2942  euind  3013  2reuswapdc  3030  reuind  3031  sbciegft  3082  rspsbc  3135  preqr2g  3887  prel12  3891  intss1  3980  intmin  3985  iinss  4059  disjiun  4120  trel3  4232  trin  4234  repizf2  4294  exmidsssnc  4335  copsexg  4379  po3nr  4450  sowlin  4460  eusvnfb  4595  reusv3  4601  ssorduni  4629  ordsucim  4642  tfis2f  4726  ssrelrel  4870  relop  4925  iss  5104  poirr2  5175  funopg  5406  funssres  5415  funun  5417  funcnvuni  5445  fv3  5713  fvmptt  5791  dff4im  5845  f1eqcocnv  5987  oprabid  6107  f1o2ndf1  6454  poxp  6458  reldmtpos  6514  rntpos  6518  smoiun  6562  tfrlem1  6569  tfrlemi1  6593  tfrexlem  6595  tfri3  6628  nntri3or  6756  qsss  6858  th3qlem1  6901  ixpsnf1o  7008  modom  7098  phplem4  7146  fimax2gtri  7196  fiintim  7228  fisseneq  7232  sbthlemi10  7273  supmoti  7323  suplub2ti  7331  ordiso2  7365  ltmpig  7696  prcdnql  7841  prcunqu  7842  recexprlem1ssl  7990  recexprlem1ssu  7991  recexprlemss1l  7992  recexprlemss1u  7993  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  caucvgprlemladdrl  8035  mulgt0sr  8135  suplocsrlem  8165  axprecex  8237  ltxrlt  8381  addid0  8689  negf1o  8699  cju  9281  nngt1ne1  9318  nnsub  9322  0mnnnnn0  9574  un0addcl  9575  un0mulcl  9576  zapne  9698  eluzuzle  9909  indstr  9972  elpq  10028  xposdif  10263  ixxdisj  10284  icodisj  10373  uzsubsubfz  10430  elfzmlbp  10517  fzofzim  10578  subfzo0  10639  addmodlteq  10813  seq3f1olemp  10930  seqf1og  10936  expcl2lemap  10966  expnegzap  10988  expaddzap  10998  expmulzap  11000  facwordi  11156  bccl  11183  hashfibclem  11260  hashfibc  11261  hashfacen  11262  hashf1lem1  11263  hashf1  11265  fundm2domnop0  11278  wrdind  11472  wrd2ind  11473  swrdccatin1  11475  swrdccatin2  11479  pfxccat3  11484  pfxccat3a  11488  swrdccat3blem  11489  reuccatpfxs1  11497  ovshftex  11562  cau3lem  11858  maxabslemval  11952  rexanre  11964  xrmaxiflemval  11994  2clim  12045  summodc  12128  fsum2dlemstep  12179  fsumiun  12222  prodmodc  12323  fprod2dlemstep  12367  odd2np1lem  12617  oddge22np1  12626  sqoddm1div8z  12631  divalglemeunn  12666  divalglemeuneg  12668  bitsfzo  12700  gcd0id  12734  divgcdcoprm0  12857  prmdvdsexpr  12906  prmfac1  12908  qnumdencl  12943  hashdvds  12977  prm23lt5  13020  pcneg  13082  prmpwdvds  13112  ctinf  13299  imasaddfnlemg  13612  mnd1id  13740  0subm  13768  insubm  13769  dfgrp3mlem  13880  gsumvalfi  14129  ringrng  14314  domnmuln0  14555  lss1d  14692  islidlm  14788  rnglidlmcl  14789  gsumfsum  14895  tgcl  15088  epttop  15114  txbas  15282  txbasval  15291  txcnp  15295  txdis1cn  15302  bldisj  15425  reopnap  15570  dvfgg  15712  lgsdir2lem2  16062  gausslemma2dlem1a  16091  gausslemma2dlem3  16096  gausslemma2d  16102  2lgsoddprmlem2  16139  ushgredgedg  16381  ushgredgedgloop  16383  uhgr0v0e  16389  subumgredg2en  16426  uhgrspansubgrlem  16431  wlk1walkdom  16514  upgriswlkdc  16515  uspgr2wlkeq  16520  clwwlknonex2e  16595  bj-vtoclgft  16717  bj-charfun  16747  bj-charfunbi  16751  bj-indind  16872  bj-nntrans  16891  bj-nnelirr  16893  triap  16983