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  1312  19.33b2  1643  sbequ2  1783  sbi1v  1906  mor  2087  2euex  2132  eqneqall  2377  necon3ad  2409  necon1aidc  2418  necon4addc  2437  elnelall  2474  spcimgft  2840  spcimegft  2842  rspc  2862  rspcimdv  2869  rspc2gv  2880  euind  2951  2reuswapdc  2968  reuind  2969  sbciegft  3020  rspsbc  3072  preqr2g  3798  prel12  3802  intss1  3890  intmin  3895  iinss  3969  disjiun  4029  trel3  4140  trin  4142  repizf2  4196  exmidsssnc  4237  copsexg  4278  po3nr  4346  sowlin  4356  eusvnfb  4490  reusv3  4496  ssorduni  4524  ordsucim  4537  tfis2f  4621  ssrelrel  4764  relop  4817  iss  4993  poirr2  5063  funopg  5293  funssres  5301  funun  5303  funcnvuni  5328  fv3  5584  fvmptt  5656  dff4im  5711  f1eqcocnv  5841  oprabid  5957  f1o2ndf1  6295  poxp  6299  reldmtpos  6320  rntpos  6324  smoiun  6368  tfrlem1  6375  tfrlemi1  6399  tfrexlem  6401  tfri3  6434  nntri3or  6560  qsss  6662  th3qlem1  6705  ixpsnf1o  6804  phplem4  6925  fimax2gtri  6971  fiintim  7001  fisseneq  7004  sbthlemi10  7041  supmoti  7068  suplub2ti  7076  ordiso2  7110  ltmpig  7425  prcdnql  7570  prcunqu  7571  recexprlem1ssl  7719  recexprlem1ssu  7720  recexprlemss1l  7721  recexprlemss1u  7722  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgprlemladdrl  7764  mulgt0sr  7864  suplocsrlem  7894  axprecex  7966  ltxrlt  8111  addid0  8418  negf1o  8427  cju  9007  nngt1ne1  9044  nnsub  9048  0mnnnnn0  9300  un0addcl  9301  un0mulcl  9302  zapne  9419  eluzuzle  9628  indstr  9686  elpq  9742  xposdif  9976  ixxdisj  9997  icodisj  10086  uzsubsubfz  10141  elfzmlbp  10226  fzofzim  10283  subfzo0  10337  addmodlteq  10509  seq3f1olemp  10626  seqf1og  10632  expcl2lemap  10662  expnegzap  10684  expaddzap  10694  expmulzap  10696  facwordi  10851  bccl  10878  hashfacen  10947  ovshftex  11003  cau3lem  11298  maxabslemval  11392  rexanre  11404  xrmaxiflemval  11434  2clim  11485  summodc  11567  fsum2dlemstep  11618  fsumiun  11661  prodmodc  11762  fprod2dlemstep  11806  odd2np1lem  12056  oddge22np1  12065  sqoddm1div8z  12070  divalglemeunn  12105  divalglemeuneg  12107  bitsfzo  12139  gcd0id  12173  divgcdcoprm0  12296  prmdvdsexpr  12345  prmfac1  12347  qnumdencl  12382  hashdvds  12416  prm23lt5  12459  pcneg  12521  prmpwdvds  12551  ctinf  12674  imasaddfnlemg  13018  mnd1id  13160  0subm  13188  insubm  13189  dfgrp3mlem  13302  ringrng  13670  domnmuln0  13907  lss1d  14017  islidlm  14113  rnglidlmcl  14114  tgcl  14408  epttop  14434  txbas  14602  txbasval  14611  txcnp  14615  txdis1cn  14622  bldisj  14745  reopnap  14890  dvfgg  15032  lgsdir2lem2  15378  gausslemma2dlem1a  15407  gausslemma2dlem3  15412  gausslemma2d  15418  2lgsoddprmlem2  15455  bj-vtoclgft  15529  bj-charfun  15561  bj-charfunbi  15565  bj-indind  15686  bj-nntrans  15705  bj-nnelirr  15707  triap  15786