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  2880  spcimegft  2882  rspc  2902  rspcimdv  2909  rspc2gv  2920  euind  2991  2reuswapdc  3008  reuind  3009  sbciegft  3060  rspsbc  3113  preqr2g  3848  prel12  3852  intss1  3941  intmin  3946  iinss  4020  disjiun  4081  trel3  4193  trin  4195  repizf2  4250  exmidsssnc  4291  copsexg  4334  po3nr  4405  sowlin  4415  eusvnfb  4549  reusv3  4555  ssorduni  4583  ordsucim  4596  tfis2f  4680  ssrelrel  4824  relop  4878  iss  5057  poirr2  5127  funopg  5358  funssres  5366  funun  5368  funcnvuni  5396  fv3  5658  fvmptt  5734  dff4im  5789  f1eqcocnv  5927  oprabid  6045  f1o2ndf1  6388  poxp  6392  reldmtpos  6414  rntpos  6418  smoiun  6462  tfrlem1  6469  tfrlemi1  6493  tfrexlem  6495  tfri3  6528  nntri3or  6656  qsss  6758  th3qlem1  6801  ixpsnf1o  6900  modom  6989  phplem4  7036  fimax2gtri  7084  fiintim  7116  fisseneq  7119  sbthlemi10  7156  supmoti  7183  suplub2ti  7191  ordiso2  7225  ltmpig  7549  prcdnql  7694  prcunqu  7695  recexprlem1ssl  7843  recexprlem1ssu  7844  recexprlemss1l  7845  recexprlemss1u  7846  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgprlemladdrl  7888  mulgt0sr  7988  suplocsrlem  8018  axprecex  8090  ltxrlt  8235  addid0  8542  negf1o  8551  cju  9131  nngt1ne1  9168  nnsub  9172  0mnnnnn0  9424  un0addcl  9425  un0mulcl  9426  zapne  9544  eluzuzle  9754  indstr  9817  elpq  9873  xposdif  10107  ixxdisj  10128  icodisj  10217  uzsubsubfz  10272  elfzmlbp  10357  fzofzim  10417  subfzo0  10478  addmodlteq  10650  seq3f1olemp  10767  seqf1og  10773  expcl2lemap  10803  expnegzap  10825  expaddzap  10835  expmulzap  10837  facwordi  10992  bccl  11019  hashfacen  11090  fundm2domnop0  11099  wrdind  11293  wrd2ind  11294  swrdccatin1  11296  swrdccatin2  11300  pfxccat3  11305  pfxccat3a  11309  swrdccat3blem  11310  reuccatpfxs1  11318  ovshftex  11370  cau3lem  11665  maxabslemval  11759  rexanre  11771  xrmaxiflemval  11801  2clim  11852  summodc  11934  fsum2dlemstep  11985  fsumiun  12028  prodmodc  12129  fprod2dlemstep  12173  odd2np1lem  12423  oddge22np1  12432  sqoddm1div8z  12437  divalglemeunn  12472  divalglemeuneg  12474  bitsfzo  12506  gcd0id  12540  divgcdcoprm0  12663  prmdvdsexpr  12712  prmfac1  12714  qnumdencl  12749  hashdvds  12783  prm23lt5  12826  pcneg  12888  prmpwdvds  12918  ctinf  13041  imasaddfnlemg  13387  mnd1id  13529  0subm  13557  insubm  13558  dfgrp3mlem  13671  ringrng  14039  domnmuln0  14277  lss1d  14387  islidlm  14483  rnglidlmcl  14484  tgcl  14778  epttop  14804  txbas  14972  txbasval  14981  txcnp  14985  txdis1cn  14992  bldisj  15115  reopnap  15260  dvfgg  15402  lgsdir2lem2  15748  gausslemma2dlem1a  15777  gausslemma2dlem3  15782  gausslemma2d  15788  2lgsoddprmlem2  15825  ushgredgedg  16065  ushgredgedgloop  16067  uhgr0v0e  16073  wlk1walkdom  16156  upgriswlkdc  16157  uspgr2wlkeq  16162  clwwlknonex2e  16235  bj-vtoclgft  16307  bj-charfun  16338  bj-charfunbi  16342  bj-indind  16463  bj-nntrans  16482  bj-nnelirr  16484  triap  16569