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  3844  prel12  3848  intss1  3937  intmin  3942  iinss  4016  disjiun  4077  trel3  4189  trin  4191  repizf2  4245  exmidsssnc  4286  copsexg  4329  po3nr  4400  sowlin  4410  eusvnfb  4544  reusv3  4550  ssorduni  4578  ordsucim  4591  tfis2f  4675  ssrelrel  4818  relop  4871  iss  5050  poirr2  5120  funopg  5351  funssres  5359  funun  5361  funcnvuni  5389  fv3  5649  fvmptt  5725  dff4im  5780  f1eqcocnv  5914  oprabid  6032  f1o2ndf1  6372  poxp  6376  reldmtpos  6397  rntpos  6401  smoiun  6445  tfrlem1  6452  tfrlemi1  6476  tfrexlem  6478  tfri3  6511  nntri3or  6637  qsss  6739  th3qlem1  6782  ixpsnf1o  6881  phplem4  7012  fimax2gtri  7059  fiintim  7089  fisseneq  7092  sbthlemi10  7129  supmoti  7156  suplub2ti  7164  ordiso2  7198  ltmpig  7522  prcdnql  7667  prcunqu  7668  recexprlem1ssl  7816  recexprlem1ssu  7817  recexprlemss1l  7818  recexprlemss1u  7819  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  caucvgprlemladdrl  7861  mulgt0sr  7961  suplocsrlem  7991  axprecex  8063  ltxrlt  8208  addid0  8515  negf1o  8524  cju  9104  nngt1ne1  9141  nnsub  9145  0mnnnnn0  9397  un0addcl  9398  un0mulcl  9399  zapne  9517  eluzuzle  9726  indstr  9784  elpq  9840  xposdif  10074  ixxdisj  10095  icodisj  10184  uzsubsubfz  10239  elfzmlbp  10324  fzofzim  10384  subfzo0  10443  addmodlteq  10615  seq3f1olemp  10732  seqf1og  10738  expcl2lemap  10768  expnegzap  10790  expaddzap  10800  expmulzap  10802  facwordi  10957  bccl  10984  hashfacen  11053  fundm2domnop0  11062  wrdind  11249  wrd2ind  11250  swrdccatin1  11252  swrdccatin2  11256  pfxccat3  11261  pfxccat3a  11265  swrdccat3blem  11266  reuccatpfxs1  11274  ovshftex  11325  cau3lem  11620  maxabslemval  11714  rexanre  11726  xrmaxiflemval  11756  2clim  11807  summodc  11889  fsum2dlemstep  11940  fsumiun  11983  prodmodc  12084  fprod2dlemstep  12128  odd2np1lem  12378  oddge22np1  12387  sqoddm1div8z  12392  divalglemeunn  12427  divalglemeuneg  12429  bitsfzo  12461  gcd0id  12495  divgcdcoprm0  12618  prmdvdsexpr  12667  prmfac1  12669  qnumdencl  12704  hashdvds  12738  prm23lt5  12781  pcneg  12843  prmpwdvds  12873  ctinf  12996  imasaddfnlemg  13342  mnd1id  13484  0subm  13512  insubm  13513  dfgrp3mlem  13626  ringrng  13994  domnmuln0  14231  lss1d  14341  islidlm  14437  rnglidlmcl  14438  tgcl  14732  epttop  14758  txbas  14926  txbasval  14935  txcnp  14939  txdis1cn  14946  bldisj  15069  reopnap  15214  dvfgg  15356  lgsdir2lem2  15702  gausslemma2dlem1a  15731  gausslemma2dlem3  15736  gausslemma2d  15742  2lgsoddprmlem2  15779  ushgredgedg  16018  ushgredgedgloop  16020  bj-vtoclgft  16097  bj-charfun  16128  bj-charfunbi  16132  bj-indind  16253  bj-nntrans  16272  bj-nnelirr  16274  triap  16356