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 ⊢ (𝜒 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr4g  205  ancomsd  269  pm2.13dc  897  3jao  1342  19.33b2  1682  sbequ2  1822  sbi1v  1946  mor  2129  2euex  2174  eqneqall  2430  necon3ad  2462  necon1aidc  2471  necon4addc  2490  elnelall  2527  spcimgft  2901  spcimegft  2903  rspc  2923  rspcimdv  2930  rspc2gv  2942  euind  3013  2reuswapdc  3030  reuind  3031  sbciegft  3082  rspsbc  3135  preqr2g  3892  prel12  3896  intss1  3985  intmin  3990  iinss  4064  disjiun  4125  trel3  4237  trin  4239  repizf2  4299  exmidsssnc  4340  copsexg  4384  po3nr  4455  sowlin  4465  eusvnfb  4600  reusv3  4606  ssorduni  4634  ordsucim  4647  tfis2f  4731  ssrelrel  4875  relop  4930  iss  5109  poirr2  5180  funopg  5411  funssres  5420  funun  5422  funcnvuni  5450  fv3  5718  fvmptt  5797  dff4im  5854  f1eqcocnv  5997  oprabid  6117  f1o2ndf1  6464  poxp  6468  reldmtpos  6524  rntpos  6528  smoiun  6572  tfrlem1  6579  tfrlemi1  6603  tfrexlem  6605  tfri3  6638  nntri3or  6766  qsss  6868  th3qlem1  6911  ixpsnf1o  7018  modom  7108  phplem4  7156  fimax2gtri  7206  fiintim  7238  fisseneq  7242  sbthlemi10  7283  supmoti  7334  suplub2ti  7342  ordiso2  7376  ltmpig  7707  prcdnql  7852  prcunqu  7853  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1l  8003  recexprlemss1u  8004  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemladdrl  8046  mulgt0sr  8146  suplocsrlem  8176  axprecex  8248  ltxrlt  8392  addid0  8701  negf1o  8711  cju  9294  nngt1ne1  9342  nnsub  9346  0mnnnnn0  9600  un0addcl  9601  un0mulcl  9602  zapne  9724  eluzuzle  9940  indstr  10003  elpq  10060  xposdif  10295  ixxdisj  10316  icodisj  10405  uzsubsubfz  10463  elfzmlbp  10550  fzofzim  10611  subfzo0  10672  addmodlteq  10850  seq3f1olemp  10967  seqf1og  10973  expcl2lemap  11003  expnegzap  11025  expaddzap  11035  expmulzap  11037  facwordi  11194  bccl  11221  hashfibclem  11298  hashfibc  11299  hashfacen  11300  hashf1lem1  11301  hashf1  11303  fundm2domnop0  11316  wrdind  11510  wrd2ind  11511  swrdccatin1  11513  swrdccatin2  11517  pfxccat3  11522  pfxccat3a  11526  swrdccat3blem  11527  reuccatpfxs1  11535  ovshftex  11600  cau3lem  11897  maxabslemval  11991  rexanre  12003  xrmaxiflemval  12035  2clim  12086  summodc  12169  fsum2dlemstep  12220  fsumiun  12263  prodmodc  12364  fprod2dlemstep  12408  odd2np1lem  12658  oddge22np1  12667  sqoddm1div8z  12672  divalglemeunn  12707  divalglemeuneg  12709  bitsfzo  12741  gcd0id  12775  divgcdcoprm0  12898  prmdvdsexpr  12948  prmfac1  12950  qnumdencl  12986  nn0sqdcq  13007  hashdvds  13022  prm23lt5  13065  pcneg  13127  prmpwdvds  13157  prmlem0  13243  ctinf  13373  imasaddfnlemg  13688  mnd1id  13816  0subm  13844  insubm  13845  dfgrp3mlem  13956  gsumvalfi  14236  ringrng  14425  domnmuln0  14666  lss1d  14804  islidlm  14900  rnglidlmcl  14901  gsumfsum  15007  tgcl  15256  epttop  15282  txbas  15450  txbasval  15459  txcnp  15463  txdis1cn  15470  bldisj  15593  reopnap  15738  dvfgg  15880  ppiublem1  16252  lgsdir2lem2  16314  gausslemma2dlem1a  16343  gausslemma2dlem3  16348  gausslemma2d  16354  2lgsoddprmlem2  16391  ushgredgedg  16633  ushgredgedgloop  16635  uhgr0v0e  16641  subumgredg2en  16678  uhgrspansubgrlem  16683  wlk1walkdom  16766  upgriswlkdc  16767  uspgr2wlkeq  16772  clwwlknonex2e  16847  bj-vtoclgft  16969  bj-charfun  16999  bj-charfunbi  17003  bj-indind  17124  bj-nntrans  17143  bj-nnelirr  17145  triap  17244