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  893  3jao  1338  19.33b2  1678  sbequ2  1817  sbi1v  1940  mor  2122  2euex  2167  eqneqall  2413  necon3ad  2445  necon1aidc  2454  necon4addc  2473  elnelall  2510  spcimgft  2883  spcimegft  2885  rspc  2905  rspcimdv  2912  rspc2gv  2923  euind  2994  2reuswapdc  3011  reuind  3012  sbciegft  3063  rspsbc  3116  preqr2g  3855  prel12  3859  intss1  3948  intmin  3953  iinss  4027  disjiun  4088  trel3  4200  trin  4202  repizf2  4258  exmidsssnc  4299  copsexg  4342  po3nr  4413  sowlin  4423  eusvnfb  4557  reusv3  4563  ssorduni  4591  ordsucim  4604  tfis2f  4688  ssrelrel  4832  relop  4886  iss  5065  poirr2  5136  funopg  5367  funssres  5376  funun  5378  funcnvuni  5406  fv3  5671  fvmptt  5747  dff4im  5801  f1eqcocnv  5942  oprabid  6060  f1o2ndf1  6402  poxp  6406  reldmtpos  6462  rntpos  6466  smoiun  6510  tfrlem1  6517  tfrlemi1  6541  tfrexlem  6543  tfri3  6576  nntri3or  6704  qsss  6806  th3qlem1  6849  ixpsnf1o  6948  modom  7037  phplem4  7084  fimax2gtri  7134  fiintim  7166  fisseneq  7170  sbthlemi10  7208  supmoti  7252  suplub2ti  7260  ordiso2  7294  ltmpig  7619  prcdnql  7764  prcunqu  7765  recexprlem1ssl  7913  recexprlem1ssu  7914  recexprlemss1l  7915  recexprlemss1u  7916  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  caucvgprlemladdrl  7958  mulgt0sr  8058  suplocsrlem  8088  axprecex  8160  ltxrlt  8304  addid0  8611  negf1o  8620  cju  9200  nngt1ne1  9237  nnsub  9241  0mnnnnn0  9493  un0addcl  9494  un0mulcl  9495  zapne  9615  eluzuzle  9825  indstr  9888  elpq  9944  xposdif  10178  ixxdisj  10199  icodisj  10288  uzsubsubfz  10344  elfzmlbp  10429  fzofzim  10490  subfzo0  10551  addmodlteq  10723  seq3f1olemp  10840  seqf1og  10846  expcl2lemap  10876  expnegzap  10898  expaddzap  10908  expmulzap  10910  facwordi  11065  bccl  11092  hashfacen  11163  fundm2domnop0  11175  wrdind  11369  wrd2ind  11370  swrdccatin1  11372  swrdccatin2  11376  pfxccat3  11381  pfxccat3a  11385  swrdccat3blem  11386  reuccatpfxs1  11394  ovshftex  11459  cau3lem  11754  maxabslemval  11848  rexanre  11860  xrmaxiflemval  11890  2clim  11941  summodc  12024  fsum2dlemstep  12075  fsumiun  12118  prodmodc  12219  fprod2dlemstep  12263  odd2np1lem  12513  oddge22np1  12522  sqoddm1div8z  12527  divalglemeunn  12562  divalglemeuneg  12564  bitsfzo  12596  gcd0id  12630  divgcdcoprm0  12753  prmdvdsexpr  12802  prmfac1  12804  qnumdencl  12839  hashdvds  12873  prm23lt5  12916  pcneg  12978  prmpwdvds  13008  ctinf  13131  imasaddfnlemg  13477  mnd1id  13619  0subm  13647  insubm  13648  dfgrp3mlem  13761  ringrng  14130  domnmuln0  14369  lss1d  14479  islidlm  14575  rnglidlmcl  14576  tgcl  14875  epttop  14901  txbas  15069  txbasval  15078  txcnp  15082  txdis1cn  15089  bldisj  15212  reopnap  15357  dvfgg  15499  lgsdir2lem2  15848  gausslemma2dlem1a  15877  gausslemma2dlem3  15882  gausslemma2d  15888  2lgsoddprmlem2  15925  ushgredgedg  16167  ushgredgedgloop  16169  uhgr0v0e  16175  subumgredg2en  16212  uhgrspansubgrlem  16217  wlk1walkdom  16300  upgriswlkdc  16301  uspgr2wlkeq  16306  clwwlknonex2e  16381  bj-vtoclgft  16493  bj-charfun  16523  bj-charfunbi  16527  bj-indind  16648  bj-nntrans  16667  bj-nnelirr  16669  triap  16761  gfsumval  16809