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  892  3jao  1337  19.33b2  1677  sbequ2  1817  sbi1v  1940  mor  2122  2euex  2167  eqneqall  2412  necon3ad  2444  necon1aidc  2453  necon4addc  2472  elnelall  2509  spcimgft  2882  spcimegft  2884  rspc  2904  rspcimdv  2911  rspc2gv  2922  euind  2993  2reuswapdc  3010  reuind  3011  sbciegft  3062  rspsbc  3115  preqr2g  3850  prel12  3854  intss1  3943  intmin  3948  iinss  4022  disjiun  4083  trel3  4195  trin  4197  repizf2  4252  exmidsssnc  4293  copsexg  4336  po3nr  4407  sowlin  4417  eusvnfb  4551  reusv3  4557  ssorduni  4585  ordsucim  4598  tfis2f  4682  ssrelrel  4826  relop  4880  iss  5059  poirr2  5129  funopg  5360  funssres  5369  funun  5371  funcnvuni  5399  fv3  5662  fvmptt  5738  dff4im  5793  f1eqcocnv  5931  oprabid  6049  f1o2ndf1  6392  poxp  6396  reldmtpos  6418  rntpos  6422  smoiun  6466  tfrlem1  6473  tfrlemi1  6497  tfrexlem  6499  tfri3  6532  nntri3or  6660  qsss  6762  th3qlem1  6805  ixpsnf1o  6904  modom  6993  phplem4  7040  fimax2gtri  7090  fiintim  7122  fisseneq  7126  sbthlemi10  7164  supmoti  7191  suplub2ti  7199  ordiso2  7233  ltmpig  7558  prcdnql  7703  prcunqu  7704  recexprlem1ssl  7852  recexprlem1ssu  7853  recexprlemss1l  7854  recexprlemss1u  7855  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgprlemladdrl  7897  mulgt0sr  7997  suplocsrlem  8027  axprecex  8099  ltxrlt  8244  addid0  8551  negf1o  8560  cju  9140  nngt1ne1  9177  nnsub  9181  0mnnnnn0  9433  un0addcl  9434  un0mulcl  9435  zapne  9553  eluzuzle  9763  indstr  9826  elpq  9882  xposdif  10116  ixxdisj  10137  icodisj  10226  uzsubsubfz  10281  elfzmlbp  10366  fzofzim  10426  subfzo0  10487  addmodlteq  10659  seq3f1olemp  10776  seqf1og  10782  expcl2lemap  10812  expnegzap  10834  expaddzap  10844  expmulzap  10846  facwordi  11001  bccl  11028  hashfacen  11099  fundm2domnop0  11108  wrdind  11302  wrd2ind  11303  swrdccatin1  11305  swrdccatin2  11309  pfxccat3  11314  pfxccat3a  11318  swrdccat3blem  11319  reuccatpfxs1  11327  ovshftex  11379  cau3lem  11674  maxabslemval  11768  rexanre  11780  xrmaxiflemval  11810  2clim  11861  summodc  11943  fsum2dlemstep  11994  fsumiun  12037  prodmodc  12138  fprod2dlemstep  12182  odd2np1lem  12432  oddge22np1  12441  sqoddm1div8z  12446  divalglemeunn  12481  divalglemeuneg  12483  bitsfzo  12515  gcd0id  12549  divgcdcoprm0  12672  prmdvdsexpr  12721  prmfac1  12723  qnumdencl  12758  hashdvds  12792  prm23lt5  12835  pcneg  12897  prmpwdvds  12927  ctinf  13050  imasaddfnlemg  13396  mnd1id  13538  0subm  13566  insubm  13567  dfgrp3mlem  13680  ringrng  14048  domnmuln0  14286  lss1d  14396  islidlm  14492  rnglidlmcl  14493  tgcl  14787  epttop  14813  txbas  14981  txbasval  14990  txcnp  14994  txdis1cn  15001  bldisj  15124  reopnap  15269  dvfgg  15411  lgsdir2lem2  15757  gausslemma2dlem1a  15786  gausslemma2dlem3  15791  gausslemma2d  15797  2lgsoddprmlem2  15834  ushgredgedg  16076  ushgredgedgloop  16078  uhgr0v0e  16084  subumgredg2en  16121  uhgrspansubgrlem  16126  wlk1walkdom  16209  upgriswlkdc  16210  uspgr2wlkeq  16215  clwwlknonex2e  16290  bj-vtoclgft  16371  bj-charfun  16402  bj-charfunbi  16406  bj-indind  16527  bj-nntrans  16546  bj-nnelirr  16548  triap  16633  gfsumval  16680