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  2879  spcimegft  2881  rspc  2901  rspcimdv  2908  rspc2gv  2919  euind  2990  2reuswapdc  3007  reuind  3008  sbciegft  3059  rspsbc  3112  preqr2g  3845  prel12  3849  intss1  3938  intmin  3943  iinss  4017  disjiun  4078  trel3  4190  trin  4192  repizf2  4247  exmidsssnc  4288  copsexg  4331  po3nr  4402  sowlin  4412  eusvnfb  4546  reusv3  4552  ssorduni  4580  ordsucim  4593  tfis2f  4677  ssrelrel  4821  relop  4875  iss  5054  poirr2  5124  funopg  5355  funssres  5363  funun  5365  funcnvuni  5393  fv3  5655  fvmptt  5731  dff4im  5786  f1eqcocnv  5924  oprabid  6042  f1o2ndf1  6385  poxp  6389  reldmtpos  6410  rntpos  6414  smoiun  6458  tfrlem1  6465  tfrlemi1  6489  tfrexlem  6491  tfri3  6524  nntri3or  6652  qsss  6754  th3qlem1  6797  ixpsnf1o  6896  phplem4  7029  fimax2gtri  7077  fiintim  7109  fisseneq  7112  sbthlemi10  7149  supmoti  7176  suplub2ti  7184  ordiso2  7218  ltmpig  7542  prcdnql  7687  prcunqu  7688  recexprlem1ssl  7836  recexprlem1ssu  7837  recexprlemss1l  7838  recexprlemss1u  7839  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  caucvgprlemladdrl  7881  mulgt0sr  7981  suplocsrlem  8011  axprecex  8083  ltxrlt  8228  addid0  8535  negf1o  8544  cju  9124  nngt1ne1  9161  nnsub  9165  0mnnnnn0  9417  un0addcl  9418  un0mulcl  9419  zapne  9537  eluzuzle  9747  indstr  9805  elpq  9861  xposdif  10095  ixxdisj  10116  icodisj  10205  uzsubsubfz  10260  elfzmlbp  10345  fzofzim  10405  subfzo0  10465  addmodlteq  10637  seq3f1olemp  10754  seqf1og  10760  expcl2lemap  10790  expnegzap  10812  expaddzap  10822  expmulzap  10824  facwordi  10979  bccl  11006  hashfacen  11076  fundm2domnop0  11085  wrdind  11275  wrd2ind  11276  swrdccatin1  11278  swrdccatin2  11282  pfxccat3  11287  pfxccat3a  11291  swrdccat3blem  11292  reuccatpfxs1  11300  ovshftex  11351  cau3lem  11646  maxabslemval  11740  rexanre  11752  xrmaxiflemval  11782  2clim  11833  summodc  11915  fsum2dlemstep  11966  fsumiun  12009  prodmodc  12110  fprod2dlemstep  12154  odd2np1lem  12404  oddge22np1  12413  sqoddm1div8z  12418  divalglemeunn  12453  divalglemeuneg  12455  bitsfzo  12487  gcd0id  12521  divgcdcoprm0  12644  prmdvdsexpr  12693  prmfac1  12695  qnumdencl  12730  hashdvds  12764  prm23lt5  12807  pcneg  12869  prmpwdvds  12899  ctinf  13022  imasaddfnlemg  13368  mnd1id  13510  0subm  13538  insubm  13539  dfgrp3mlem  13652  ringrng  14020  domnmuln0  14258  lss1d  14368  islidlm  14464  rnglidlmcl  14465  tgcl  14759  epttop  14785  txbas  14953  txbasval  14962  txcnp  14966  txdis1cn  14973  bldisj  15096  reopnap  15241  dvfgg  15383  lgsdir2lem2  15729  gausslemma2dlem1a  15758  gausslemma2dlem3  15763  gausslemma2d  15769  2lgsoddprmlem2  15806  ushgredgedg  16045  ushgredgedgloop  16047  uhgr0v0e  16053  wlk1walkdom  16131  upgriswlkdc  16132  uspgr2wlkeq  16137  bj-vtoclgft  16248  bj-charfun  16279  bj-charfunbi  16283  bj-indind  16404  bj-nntrans  16423  bj-nnelirr  16425  triap  16511