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  8700  negf1o  8710  cju  9293  nngt1ne1  9341  nnsub  9345  0mnnnnn0  9599  un0addcl  9600  un0mulcl  9601  zapne  9723  eluzuzle  9939  indstr  10002  elpq  10059  xposdif  10294  ixxdisj  10315  icodisj  10404  uzsubsubfz  10462  elfzmlbp  10549  fzofzim  10610  subfzo0  10671  addmodlteq  10848  seq3f1olemp  10965  seqf1og  10971  expcl2lemap  11001  expnegzap  11023  expaddzap  11033  expmulzap  11035  facwordi  11192  bccl  11219  hashfibclem  11296  hashfibc  11297  hashfacen  11298  hashf1lem1  11299  hashf1  11301  fundm2domnop0  11314  wrdind  11508  wrd2ind  11509  swrdccatin1  11511  swrdccatin2  11515  pfxccat3  11520  pfxccat3a  11524  swrdccat3blem  11525  reuccatpfxs1  11533  ovshftex  11598  cau3lem  11895  maxabslemval  11989  rexanre  12001  xrmaxiflemval  12032  2clim  12083  summodc  12166  fsum2dlemstep  12217  fsumiun  12260  prodmodc  12361  fprod2dlemstep  12405  odd2np1lem  12655  oddge22np1  12664  sqoddm1div8z  12669  divalglemeunn  12704  divalglemeuneg  12706  bitsfzo  12738  gcd0id  12772  divgcdcoprm0  12895  prmdvdsexpr  12945  prmfac1  12947  qnumdencl  12983  nn0sqdcq  13004  hashdvds  13019  prm23lt5  13062  pcneg  13124  prmpwdvds  13154  prmlem0  13240  ctinf  13370  imasaddfnlemg  13684  mnd1id  13812  0subm  13840  insubm  13841  dfgrp3mlem  13952  gsumvalfi  14201  ringrng  14390  domnmuln0  14631  lss1d  14769  islidlm  14865  rnglidlmcl  14866  gsumfsum  14972  tgcl  15214  epttop  15240  txbas  15408  txbasval  15417  txcnp  15421  txdis1cn  15428  bldisj  15551  reopnap  15696  dvfgg  15838  ppiublem1  16192  lgsdir2lem2  16246  gausslemma2dlem1a  16275  gausslemma2dlem3  16280  gausslemma2d  16286  2lgsoddprmlem2  16323  ushgredgedg  16565  ushgredgedgloop  16567  uhgr0v0e  16573  subumgredg2en  16610  uhgrspansubgrlem  16615  wlk1walkdom  16698  upgriswlkdc  16699  uspgr2wlkeq  16704  clwwlknonex2e  16779  bj-vtoclgft  16901  bj-charfun  16931  bj-charfunbi  16935  bj-indind  17056  bj-nntrans  17075  bj-nnelirr  17077  triap  17176