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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used 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  3892  prel12  3896  intss1  3985  intmin  3990  iinss  4064  disjiun  4125  trel3  4237  trin  4239  repizf2  4299  exmidsssnc  4340  copsexg  4384  po3nr  4455  sowlin  4465  eusvnfb  4600  reusv3  4606  ssorduni  4634  ordsucim  4647  tfis2f  4731  ssrelrel  4875  relop  4930  iss  5109  poirr2  5180  funopg  5411  funssres  5420  funun  5422  funcnvuni  5450  fv3  5718  fvmptt  5797  dff4im  5854  f1eqcocnv  5997  oprabid  6117  f1o2ndf1  6464  poxp  6468  reldmtpos  6524  rntpos  6528  smoiun  6572  tfrlem1  6579  tfrlemi1  6603  tfrexlem  6605  tfri3  6638  nntri3or  6766  qsss  6868  th3qlem1  6911  ixpsnf1o  7018  modom  7108  phplem4  7156  fimax2gtri  7206  fiintim  7238  fisseneq  7242  sbthlemi10  7283  supmoti  7333  suplub2ti  7341  ordiso2  7375  ltmpig  7706  prcdnql  7851  prcunqu  7852  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  mulgt0sr  8145  suplocsrlem  8175  axprecex  8247  ltxrlt  8391  addid0  8699  negf1o  8709  cju  9291  nngt1ne1  9339  nnsub  9343  0mnnnnn0  9595  un0addcl  9596  un0mulcl  9597  zapne  9719  eluzuzle  9930  indstr  9993  elpq  10049  xposdif  10284  ixxdisj  10305  icodisj  10394  uzsubsubfz  10452  elfzmlbp  10539  fzofzim  10600  subfzo0  10661  addmodlteq  10835  seq3f1olemp  10952  seqf1og  10958  expcl2lemap  10988  expnegzap  11010  expaddzap  11020  expmulzap  11022  facwordi  11178  bccl  11205  hashfibclem  11282  hashfibc  11283  hashfacen  11284  hashf1lem1  11285  hashf1  11287  fundm2domnop0  11300  wrdind  11494  wrd2ind  11495  swrdccatin1  11497  swrdccatin2  11501  pfxccat3  11506  pfxccat3a  11510  swrdccat3blem  11511  reuccatpfxs1  11519  ovshftex  11584  cau3lem  11880  maxabslemval  11974  rexanre  11986  xrmaxiflemval  12016  2clim  12067  summodc  12150  fsum2dlemstep  12201  fsumiun  12244  prodmodc  12345  fprod2dlemstep  12389  odd2np1lem  12639  oddge22np1  12648  sqoddm1div8z  12653  divalglemeunn  12688  divalglemeuneg  12690  bitsfzo  12722  gcd0id  12756  divgcdcoprm0  12879  prmdvdsexpr  12928  prmfac1  12930  qnumdencl  12965  hashdvds  12999  prm23lt5  13042  pcneg  13104  prmpwdvds  13134  ctinf  13321  imasaddfnlemg  13635  mnd1id  13763  0subm  13791  insubm  13792  dfgrp3mlem  13903  gsumvalfi  14152  ringrng  14341  domnmuln0  14582  lss1d  14720  islidlm  14816  rnglidlmcl  14817  gsumfsum  14923  tgcl  15165  epttop  15191  txbas  15359  txbasval  15368  txcnp  15372  txdis1cn  15379  bldisj  15502  reopnap  15647  dvfgg  15789  lgsdir2lem2  16148  gausslemma2dlem1a  16177  gausslemma2dlem3  16182  gausslemma2d  16188  2lgsoddprmlem2  16225  ushgredgedg  16467  ushgredgedgloop  16469  uhgr0v0e  16475  subumgredg2en  16512  uhgrspansubgrlem  16517  wlk1walkdom  16600  upgriswlkdc  16601  uspgr2wlkeq  16606  clwwlknonex2e  16681  bj-vtoclgft  16803  bj-charfun  16833  bj-charfunbi  16837  bj-indind  16958  bj-nntrans  16977  bj-nnelirr  16979  triap  17078