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  5932  oprabid  6050  f1o2ndf1  6393  poxp  6397  reldmtpos  6419  rntpos  6423  smoiun  6467  tfrlem1  6474  tfrlemi1  6498  tfrexlem  6500  tfri3  6533  nntri3or  6661  qsss  6763  th3qlem1  6806  ixpsnf1o  6905  modom  6994  phplem4  7041  fimax2gtri  7091  fiintim  7123  fisseneq  7127  sbthlemi10  7165  supmoti  7192  suplub2ti  7200  ordiso2  7234  ltmpig  7559  prcdnql  7704  prcunqu  7705  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1l  7855  recexprlemss1u  7856  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  mulgt0sr  7998  suplocsrlem  8028  axprecex  8100  ltxrlt  8245  addid0  8552  negf1o  8561  cju  9141  nngt1ne1  9178  nnsub  9182  0mnnnnn0  9434  un0addcl  9435  un0mulcl  9436  zapne  9554  eluzuzle  9764  indstr  9827  elpq  9883  xposdif  10117  ixxdisj  10138  icodisj  10227  uzsubsubfz  10282  elfzmlbp  10367  fzofzim  10428  subfzo0  10489  addmodlteq  10661  seq3f1olemp  10778  seqf1og  10784  expcl2lemap  10814  expnegzap  10836  expaddzap  10846  expmulzap  10848  facwordi  11003  bccl  11030  hashfacen  11101  fundm2domnop0  11113  wrdind  11307  wrd2ind  11308  swrdccatin1  11310  swrdccatin2  11314  pfxccat3  11319  pfxccat3a  11323  swrdccat3blem  11324  reuccatpfxs1  11332  ovshftex  11397  cau3lem  11692  maxabslemval  11786  rexanre  11798  xrmaxiflemval  11828  2clim  11879  summodc  11962  fsum2dlemstep  12013  fsumiun  12056  prodmodc  12157  fprod2dlemstep  12201  odd2np1lem  12451  oddge22np1  12460  sqoddm1div8z  12465  divalglemeunn  12500  divalglemeuneg  12502  bitsfzo  12534  gcd0id  12568  divgcdcoprm0  12691  prmdvdsexpr  12740  prmfac1  12742  qnumdencl  12777  hashdvds  12811  prm23lt5  12854  pcneg  12916  prmpwdvds  12946  ctinf  13069  imasaddfnlemg  13415  mnd1id  13557  0subm  13585  insubm  13586  dfgrp3mlem  13699  ringrng  14068  domnmuln0  14306  lss1d  14416  islidlm  14512  rnglidlmcl  14513  tgcl  14807  epttop  14833  txbas  15001  txbasval  15010  txcnp  15014  txdis1cn  15021  bldisj  15144  reopnap  15289  dvfgg  15431  lgsdir2lem2  15777  gausslemma2dlem1a  15806  gausslemma2dlem3  15811  gausslemma2d  15817  2lgsoddprmlem2  15854  ushgredgedg  16096  ushgredgedgloop  16098  uhgr0v0e  16104  subumgredg2en  16141  uhgrspansubgrlem  16146  wlk1walkdom  16229  upgriswlkdc  16230  uspgr2wlkeq  16235  clwwlknonex2e  16310  bj-vtoclgft  16422  bj-charfun  16453  bj-charfunbi  16457  bj-indind  16578  bj-nntrans  16597  bj-nnelirr  16599  triap  16684  gfsumval  16732