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  3890  prel12  3894  intss1  3983  intmin  3988  iinss  4062  disjiun  4123  trel3  4235  trin  4237  repizf2  4297  exmidsssnc  4338  copsexg  4382  po3nr  4453  sowlin  4463  eusvnfb  4598  reusv3  4604  ssorduni  4632  ordsucim  4645  tfis2f  4729  ssrelrel  4873  relop  4928  iss  5107  poirr2  5178  funopg  5409  funssres  5418  funun  5420  funcnvuni  5448  fv3  5716  fvmptt  5794  dff4im  5848  f1eqcocnv  5991  oprabid  6111  f1o2ndf1  6458  poxp  6462  reldmtpos  6518  rntpos  6522  smoiun  6566  tfrlem1  6573  tfrlemi1  6597  tfrexlem  6599  tfri3  6632  nntri3or  6760  qsss  6862  th3qlem1  6905  ixpsnf1o  7012  modom  7102  phplem4  7150  fimax2gtri  7200  fiintim  7232  fisseneq  7236  sbthlemi10  7277  supmoti  7327  suplub2ti  7335  ordiso2  7369  ltmpig  7700  prcdnql  7845  prcunqu  7846  recexprlem1ssl  7994  recexprlem1ssu  7995  recexprlemss1l  7996  recexprlemss1u  7997  cauappcvgprlemladdru  8017  cauappcvgprlemladdrl  8018  caucvgprlemladdrl  8039  mulgt0sr  8139  suplocsrlem  8169  axprecex  8241  ltxrlt  8385  addid0  8693  negf1o  8703  cju  9285  nngt1ne1  9322  nnsub  9326  0mnnnnn0  9578  un0addcl  9579  un0mulcl  9580  zapne  9702  eluzuzle  9913  indstr  9976  elpq  10032  xposdif  10267  ixxdisj  10288  icodisj  10377  uzsubsubfz  10435  elfzmlbp  10522  fzofzim  10583  subfzo0  10644  addmodlteq  10818  seq3f1olemp  10935  seqf1og  10941  expcl2lemap  10971  expnegzap  10993  expaddzap  11003  expmulzap  11005  facwordi  11161  bccl  11188  hashfibclem  11265  hashfibc  11266  hashfacen  11267  hashf1lem1  11268  hashf1  11270  fundm2domnop0  11283  wrdind  11477  wrd2ind  11478  swrdccatin1  11480  swrdccatin2  11484  pfxccat3  11489  pfxccat3a  11493  swrdccat3blem  11494  reuccatpfxs1  11502  ovshftex  11567  cau3lem  11863  maxabslemval  11957  rexanre  11969  xrmaxiflemval  11999  2clim  12050  summodc  12133  fsum2dlemstep  12184  fsumiun  12227  prodmodc  12328  fprod2dlemstep  12372  odd2np1lem  12622  oddge22np1  12631  sqoddm1div8z  12636  divalglemeunn  12671  divalglemeuneg  12673  bitsfzo  12705  gcd0id  12739  divgcdcoprm0  12862  prmdvdsexpr  12911  prmfac1  12913  qnumdencl  12948  hashdvds  12982  prm23lt5  13025  pcneg  13087  prmpwdvds  13117  ctinf  13304  imasaddfnlemg  13618  mnd1id  13746  0subm  13774  insubm  13775  dfgrp3mlem  13886  gsumvalfi  14135  ringrng  14324  domnmuln0  14565  lss1d  14703  islidlm  14799  rnglidlmcl  14800  gsumfsum  14906  tgcl  15148  epttop  15174  txbas  15342  txbasval  15351  txcnp  15355  txdis1cn  15362  bldisj  15485  reopnap  15630  dvfgg  15772  lgsdir2lem2  16131  gausslemma2dlem1a  16160  gausslemma2dlem3  16165  gausslemma2d  16171  2lgsoddprmlem2  16208  ushgredgedg  16450  ushgredgedgloop  16452  uhgr0v0e  16458  subumgredg2en  16495  uhgrspansubgrlem  16500  wlk1walkdom  16583  upgriswlkdc  16584  uspgr2wlkeq  16589  clwwlknonex2e  16664  bj-vtoclgft  16786  bj-charfun  16816  bj-charfunbi  16820  bj-indind  16941  bj-nntrans  16960  bj-nnelirr  16962  triap  17053