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  886  3jao  1313  19.33b2  1651  sbequ2  1791  sbi1v  1914  mor  2095  2euex  2140  eqneqall  2385  necon3ad  2417  necon1aidc  2426  necon4addc  2445  elnelall  2482  spcimgft  2848  spcimegft  2850  rspc  2870  rspcimdv  2877  rspc2gv  2888  euind  2959  2reuswapdc  2976  reuind  2977  sbciegft  3028  rspsbc  3080  preqr2g  3807  prel12  3811  intss1  3899  intmin  3904  iinss  3978  disjiun  4038  trel3  4149  trin  4151  repizf2  4205  exmidsssnc  4246  copsexg  4287  po3nr  4356  sowlin  4366  eusvnfb  4500  reusv3  4506  ssorduni  4534  ordsucim  4547  tfis2f  4631  ssrelrel  4774  relop  4827  iss  5004  poirr2  5074  funopg  5304  funssres  5312  funun  5314  funcnvuni  5342  fv3  5598  fvmptt  5670  dff4im  5725  f1eqcocnv  5859  oprabid  5975  f1o2ndf1  6313  poxp  6317  reldmtpos  6338  rntpos  6342  smoiun  6386  tfrlem1  6393  tfrlemi1  6417  tfrexlem  6419  tfri3  6452  nntri3or  6578  qsss  6680  th3qlem1  6723  ixpsnf1o  6822  phplem4  6951  fimax2gtri  6997  fiintim  7027  fisseneq  7030  sbthlemi10  7067  supmoti  7094  suplub2ti  7102  ordiso2  7136  ltmpig  7451  prcdnql  7596  prcunqu  7597  recexprlem1ssl  7745  recexprlem1ssu  7746  recexprlemss1l  7747  recexprlemss1u  7748  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  caucvgprlemladdrl  7790  mulgt0sr  7890  suplocsrlem  7920  axprecex  7992  ltxrlt  8137  addid0  8444  negf1o  8453  cju  9033  nngt1ne1  9070  nnsub  9074  0mnnnnn0  9326  un0addcl  9327  un0mulcl  9328  zapne  9446  eluzuzle  9655  indstr  9713  elpq  9769  xposdif  10003  ixxdisj  10024  icodisj  10113  uzsubsubfz  10168  elfzmlbp  10253  fzofzim  10310  subfzo0  10369  addmodlteq  10541  seq3f1olemp  10658  seqf1og  10664  expcl2lemap  10694  expnegzap  10716  expaddzap  10726  expmulzap  10728  facwordi  10883  bccl  10910  hashfacen  10979  fundm2domnop0  10988  ovshftex  11072  cau3lem  11367  maxabslemval  11461  rexanre  11473  xrmaxiflemval  11503  2clim  11554  summodc  11636  fsum2dlemstep  11687  fsumiun  11730  prodmodc  11831  fprod2dlemstep  11875  odd2np1lem  12125  oddge22np1  12134  sqoddm1div8z  12139  divalglemeunn  12174  divalglemeuneg  12176  bitsfzo  12208  gcd0id  12242  divgcdcoprm0  12365  prmdvdsexpr  12414  prmfac1  12416  qnumdencl  12451  hashdvds  12485  prm23lt5  12528  pcneg  12590  prmpwdvds  12620  ctinf  12743  imasaddfnlemg  13088  mnd1id  13230  0subm  13258  insubm  13259  dfgrp3mlem  13372  ringrng  13740  domnmuln0  13977  lss1d  14087  islidlm  14183  rnglidlmcl  14184  tgcl  14478  epttop  14504  txbas  14672  txbasval  14681  txcnp  14685  txdis1cn  14692  bldisj  14815  reopnap  14960  dvfgg  15102  lgsdir2lem2  15448  gausslemma2dlem1a  15477  gausslemma2dlem3  15482  gausslemma2d  15488  2lgsoddprmlem2  15525  bj-vtoclgft  15644  bj-charfun  15676  bj-charfunbi  15680  bj-indind  15801  bj-nntrans  15820  bj-nnelirr  15822  triap  15901