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  887  3jao  1314  19.33b2  1653  sbequ2  1793  sbi1v  1916  mor  2097  2euex  2142  eqneqall  2387  necon3ad  2419  necon1aidc  2428  necon4addc  2447  elnelall  2484  spcimgft  2853  spcimegft  2855  rspc  2875  rspcimdv  2882  rspc2gv  2893  euind  2964  2reuswapdc  2981  reuind  2982  sbciegft  3033  rspsbc  3085  preqr2g  3814  prel12  3818  intss1  3906  intmin  3911  iinss  3985  disjiun  4046  trel3  4158  trin  4160  repizf2  4214  exmidsssnc  4255  copsexg  4296  po3nr  4365  sowlin  4375  eusvnfb  4509  reusv3  4515  ssorduni  4543  ordsucim  4556  tfis2f  4640  ssrelrel  4783  relop  4836  iss  5014  poirr2  5084  funopg  5314  funssres  5322  funun  5324  funcnvuni  5352  fv3  5612  fvmptt  5684  dff4im  5739  f1eqcocnv  5873  oprabid  5989  f1o2ndf1  6327  poxp  6331  reldmtpos  6352  rntpos  6356  smoiun  6400  tfrlem1  6407  tfrlemi1  6431  tfrexlem  6433  tfri3  6466  nntri3or  6592  qsss  6694  th3qlem1  6737  ixpsnf1o  6836  phplem4  6967  fimax2gtri  7013  fiintim  7043  fisseneq  7046  sbthlemi10  7083  supmoti  7110  suplub2ti  7118  ordiso2  7152  ltmpig  7472  prcdnql  7617  prcunqu  7618  recexprlem1ssl  7766  recexprlem1ssu  7767  recexprlemss1l  7768  recexprlemss1u  7769  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  caucvgprlemladdrl  7811  mulgt0sr  7911  suplocsrlem  7941  axprecex  8013  ltxrlt  8158  addid0  8465  negf1o  8474  cju  9054  nngt1ne1  9091  nnsub  9095  0mnnnnn0  9347  un0addcl  9348  un0mulcl  9349  zapne  9467  eluzuzle  9676  indstr  9734  elpq  9790  xposdif  10024  ixxdisj  10045  icodisj  10134  uzsubsubfz  10189  elfzmlbp  10274  fzofzim  10334  subfzo0  10393  addmodlteq  10565  seq3f1olemp  10682  seqf1og  10688  expcl2lemap  10718  expnegzap  10740  expaddzap  10750  expmulzap  10752  facwordi  10907  bccl  10934  hashfacen  11003  fundm2domnop0  11012  wrdind  11198  wrd2ind  11199  ovshftex  11205  cau3lem  11500  maxabslemval  11594  rexanre  11606  xrmaxiflemval  11636  2clim  11687  summodc  11769  fsum2dlemstep  11820  fsumiun  11863  prodmodc  11964  fprod2dlemstep  12008  odd2np1lem  12258  oddge22np1  12267  sqoddm1div8z  12272  divalglemeunn  12307  divalglemeuneg  12309  bitsfzo  12341  gcd0id  12375  divgcdcoprm0  12498  prmdvdsexpr  12547  prmfac1  12549  qnumdencl  12584  hashdvds  12618  prm23lt5  12661  pcneg  12723  prmpwdvds  12753  ctinf  12876  imasaddfnlemg  13221  mnd1id  13363  0subm  13391  insubm  13392  dfgrp3mlem  13505  ringrng  13873  domnmuln0  14110  lss1d  14220  islidlm  14316  rnglidlmcl  14317  tgcl  14611  epttop  14637  txbas  14805  txbasval  14814  txcnp  14818  txdis1cn  14825  bldisj  14948  reopnap  15093  dvfgg  15235  lgsdir2lem2  15581  gausslemma2dlem1a  15610  gausslemma2dlem3  15615  gausslemma2d  15621  2lgsoddprmlem2  15658  bj-vtoclgft  15850  bj-charfun  15881  bj-charfunbi  15885  bj-indind  16006  bj-nntrans  16025  bj-nnelirr  16027  triap  16109