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 ⊢ (𝜒 → (𝜑 → 𝜃))

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  890  3jao  1335  19.33b2  1675  sbequ2  1815  sbi1v  1938  mor  2120  2euex  2165  eqneqall  2410  necon3ad  2442  necon1aidc  2451  necon4addc  2470  elnelall  2507  spcimgft  2879  spcimegft  2881  rspc  2901  rspcimdv  2908  rspc2gv  2919  euind  2990  2reuswapdc  3007  reuind  3008  sbciegft  3059  rspsbc  3112  preqr2g  3845  prel12  3849  intss1  3938  intmin  3943  iinss  4017  disjiun  4078  trel3  4190  trin  4192  repizf2  4246  exmidsssnc  4287  copsexg  4330  po3nr  4401  sowlin  4411  eusvnfb  4545  reusv3  4551  ssorduni  4579  ordsucim  4592  tfis2f  4676  ssrelrel  4819  relop  4872  iss  5051  poirr2  5121  funopg  5352  funssres  5360  funun  5362  funcnvuni  5390  fv3  5652  fvmptt  5728  dff4im  5783  f1eqcocnv  5921  oprabid  6039  f1o2ndf1  6380  poxp  6384  reldmtpos  6405  rntpos  6409  smoiun  6453  tfrlem1  6460  tfrlemi1  6484  tfrexlem  6486  tfri3  6519  nntri3or  6647  qsss  6749  th3qlem1  6792  ixpsnf1o  6891  phplem4  7024  fimax2gtri  7072  fiintim  7104  fisseneq  7107  sbthlemi10  7144  supmoti  7171  suplub2ti  7179  ordiso2  7213  ltmpig  7537  prcdnql  7682  prcunqu  7683  recexprlem1ssl  7831  recexprlem1ssu  7832  recexprlemss1l  7833  recexprlemss1u  7834  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemladdrl  7876  mulgt0sr  7976  suplocsrlem  8006  axprecex  8078  ltxrlt  8223  addid0  8530  negf1o  8539  cju  9119  nngt1ne1  9156  nnsub  9160  0mnnnnn0  9412  un0addcl  9413  un0mulcl  9414  zapne  9532  eluzuzle  9742  indstr  9800  elpq  9856  xposdif  10090  ixxdisj  10111  icodisj  10200  uzsubsubfz  10255  elfzmlbp  10340  fzofzim  10400  subfzo0  10460  addmodlteq  10632  seq3f1olemp  10749  seqf1og  10755  expcl2lemap  10785  expnegzap  10807  expaddzap  10817  expmulzap  10819  facwordi  10974  bccl  11001  hashfacen  11071  fundm2domnop0  11080  wrdind  11269  wrd2ind  11270  swrdccatin1  11272  swrdccatin2  11276  pfxccat3  11281  pfxccat3a  11285  swrdccat3blem  11286  reuccatpfxs1  11294  ovshftex  11345  cau3lem  11640  maxabslemval  11734  rexanre  11746  xrmaxiflemval  11776  2clim  11827  summodc  11909  fsum2dlemstep  11960  fsumiun  12003  prodmodc  12104  fprod2dlemstep  12148  odd2np1lem  12398  oddge22np1  12407  sqoddm1div8z  12412  divalglemeunn  12447  divalglemeuneg  12449  bitsfzo  12481  gcd0id  12515  divgcdcoprm0  12638  prmdvdsexpr  12687  prmfac1  12689  qnumdencl  12724  hashdvds  12758  prm23lt5  12801  pcneg  12863  prmpwdvds  12893  ctinf  13016  imasaddfnlemg  13362  mnd1id  13504  0subm  13532  insubm  13533  dfgrp3mlem  13646  ringrng  14014  domnmuln0  14252  lss1d  14362  islidlm  14458  rnglidlmcl  14459  tgcl  14753  epttop  14779  txbas  14947  txbasval  14956  txcnp  14960  txdis1cn  14967  bldisj  15090  reopnap  15235  dvfgg  15377  lgsdir2lem2  15723  gausslemma2dlem1a  15752  gausslemma2dlem3  15757  gausslemma2d  15763  2lgsoddprmlem2  15800  ushgredgedg  16039  ushgredgedgloop  16041  wlk1walkdom  16100  upgriswlkdc  16101  uspgr2wlkeq  16106  bj-vtoclgft  16194  bj-charfun  16225  bj-charfunbi  16229  bj-indind  16350  bj-nntrans  16369  bj-nnelirr  16371  triap  16457