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	⊢ (𝜑 ↔ 𝜓)
biimtrid.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
biimtrid	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem biimtrid

Step	Hyp	Ref	Expression
1		biimtrid.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 120	. 2 ⊢ (𝜑 → 𝜓)
3		biimtrid.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 32	1 ⊢ (𝜒 → (𝜑 → 𝜃))

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  4239  trin  4241  repizf2  4301  exmidsssnc  4342  copsexg  4386  po3nr  4457  sowlin  4467  eusvnfb  4602  reusv3  4608  ssorduni  4636  ordsucim  4649  tfis2f  4733  ssrelrel  4877  relop  4932  iss  5112  poirr2  5183  funopg  5414  funssres  5423  funun  5425  funcnvuni  5453  fv3  5721  fvmptt  5800  dff4im  5857  f1eqcocnv  6000  oprabid  6120  f1o2ndf1  6468  poxp  6472  reldmtpos  6528  rntpos  6532  smoiun  6576  tfrlem1  6583  tfrlemi1  6607  tfrexlem  6609  tfri3  6642  nntri3or  6770  qsss  6872  th3qlem1  6915  ixpsnf1o  7022  modom  7112  phplem4  7160  fimax2gtri  7210  fiintim  7242  fisseneq  7246  sbthlemi10  7288  supmoti  7339  suplub2ti  7347  ordiso2  7381  ltmpig  7712  prcdnql  7857  prcunqu  7858  recexprlem1ssl  8006  recexprlem1ssu  8007  recexprlemss1l  8008  recexprlemss1u  8009  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  mulgt0sr  8151  suplocsrlem  8181  axprecex  8253  ltxrlt  8397  addid0  8706  negf1o  8716  cju  9299  nngt1ne1  9348  nnsub  9352  0mnnnnn0  9606  un0addcl  9607  un0mulcl  9608  zapne  9730  eluzuzle  9946  indstr  10009  elpq  10066  xposdif  10301  ixxdisj  10322  icodisj  10411  uzsubsubfz  10469  elfzmlbp  10556  fzofzim  10617  subfzo0  10678  addmodlteq  10856  seq3f1olemp  10973  seqf1og  10979  expcl2lemap  11009  expnegzap  11031  expaddzap  11041  expmulzap  11043  facwordi  11200  bccl  11227  hashfibclem  11304  hashfibc  11305  hashfacen  11306  hashf1lem1  11307  hashf1  11309  fundm2domnop0  11322  wrdind  11516  wrd2ind  11517  swrdccatin1  11519  swrdccatin2  11523  pfxccat3  11528  pfxccat3a  11532  swrdccat3blem  11533  reuccatpfxs1  11541  ovshftex  11606  cau3lem  11903  maxabslemval  11997  rexanre  12009  xrmaxiflemval  12041  2clim  12092  summodc  12175  fsum2dlemstep  12226  fsumiun  12269  prodmodc  12370  fprod2dlemstep  12414  odd2np1lem  12664  oddge22np1  12673  sqoddm1div8z  12678  divalglemeunn  12713  divalglemeuneg  12715  bitsfzo  12747  gcd0id  12781  divgcdcoprm0  12904  prmdvdsexpr  12954  prmfac1  12956  qnumdencl  12992  nn0sqdcq  13013  hashdvds  13028  prm23lt5  13071  pcneg  13133  prmpwdvds  13163  prmlem0  13249  ctinf  13379  imasaddfnlemg  13694  mnd1id  13822  0subm  13850  insubm  13851  dfgrp3mlem  13962  gsumvalfi  14242  gsum2d2fi  14274  ringrng  14448  domnmuln0  14691  lss1d  14829  islidlm  14925  rnglidlmcl  14926  gsumfsum  15032  tgcl  15290  epttop  15316  txbas  15484  txbasval  15493  txcnp  15497  txdis1cn  15504  bldisj  15627  reopnap  15772  dvfgg  15914  rpcxpmul2z  16148  ppiublem1  16291  lgsdir2lem2  16353  gausslemma2dlem1a  16382  gausslemma2dlem3  16387  gausslemma2d  16393  2lgsoddprmlem2  16430  ushgredgedg  16672  ushgredgedgloop  16674  uhgr0v0e  16680  subumgredg2en  16717  uhgrspansubgrlem  16722  wlk1walkdom  16805  upgriswlkdc  16806  uspgr2wlkeq  16811  clwwlknonex2e  16886  bj-vtoclgft  17008  bj-charfun  17038  bj-charfunbi  17042  bj-indind  17163  bj-nntrans  17182  bj-nnelirr  17184  triap  17284