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  886  3jao  1313  19.33b2  1651  sbequ2  1791  sbi1v  1914  mor  2095  2euex  2140  eqneqall  2385  necon3ad  2417  necon1aidc  2426  necon4addc  2445  elnelall  2482  spcimgft  2848  spcimegft  2850  rspc  2870  rspcimdv  2877  rspc2gv  2888  euind  2959  2reuswapdc  2976  reuind  2977  sbciegft  3028  rspsbc  3080  preqr2g  3807  prel12  3811  intss1  3899  intmin  3904  iinss  3978  disjiun  4038  trel3  4149  trin  4151  repizf2  4205  exmidsssnc  4246  copsexg  4287  po3nr  4356  sowlin  4366  eusvnfb  4500  reusv3  4506  ssorduni  4534  ordsucim  4547  tfis2f  4631  ssrelrel  4774  relop  4827  iss  5004  poirr2  5074  funopg  5304  funssres  5312  funun  5314  funcnvuni  5342  fv3  5598  fvmptt  5670  dff4im  5725  f1eqcocnv  5859  oprabid  5975  f1o2ndf1  6313  poxp  6317  reldmtpos  6338  rntpos  6342  smoiun  6386  tfrlem1  6393  tfrlemi1  6417  tfrexlem  6419  tfri3  6452  nntri3or  6578  qsss  6680  th3qlem1  6723  ixpsnf1o  6822  phplem4  6951  fimax2gtri  6997  fiintim  7027  fisseneq  7030  sbthlemi10  7067  supmoti  7094  suplub2ti  7102  ordiso2  7136  ltmpig  7451  prcdnql  7596  prcunqu  7597  recexprlem1ssl  7745  recexprlem1ssu  7746  recexprlemss1l  7747  recexprlemss1u  7748  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  caucvgprlemladdrl  7790  mulgt0sr  7890  suplocsrlem  7920  axprecex  7992  ltxrlt  8137  addid0  8444  negf1o  8453  cju  9033  nngt1ne1  9070  nnsub  9074  0mnnnnn0  9326  un0addcl  9327  un0mulcl  9328  zapne  9446  eluzuzle  9655  indstr  9713  elpq  9769  xposdif  10003  ixxdisj  10024  icodisj  10113  uzsubsubfz  10168  elfzmlbp  10253  fzofzim  10310  subfzo0  10369  addmodlteq  10541  seq3f1olemp  10658  seqf1og  10664  expcl2lemap  10694  expnegzap  10716  expaddzap  10726  expmulzap  10728  facwordi  10883  bccl  10910  hashfacen  10979  fundm2domnop0  10988  ovshftex  11101  cau3lem  11396  maxabslemval  11490  rexanre  11502  xrmaxiflemval  11532  2clim  11583  summodc  11665  fsum2dlemstep  11716  fsumiun  11759  prodmodc  11860  fprod2dlemstep  11904  odd2np1lem  12154  oddge22np1  12163  sqoddm1div8z  12168  divalglemeunn  12203  divalglemeuneg  12205  bitsfzo  12237  gcd0id  12271  divgcdcoprm0  12394  prmdvdsexpr  12443  prmfac1  12445  qnumdencl  12480  hashdvds  12514  prm23lt5  12557  pcneg  12619  prmpwdvds  12649  ctinf  12772  imasaddfnlemg  13117  mnd1id  13259  0subm  13287  insubm  13288  dfgrp3mlem  13401  ringrng  13769  domnmuln0  14006  lss1d  14116  islidlm  14212  rnglidlmcl  14213  tgcl  14507  epttop  14533  txbas  14701  txbasval  14710  txcnp  14714  txdis1cn  14721  bldisj  14844  reopnap  14989  dvfgg  15131  lgsdir2lem2  15477  gausslemma2dlem1a  15506  gausslemma2dlem3  15511  gausslemma2d  15517  2lgsoddprmlem2  15554  bj-vtoclgft  15673  bj-charfun  15705  bj-charfunbi  15709  bj-indind  15830  bj-nntrans  15849  bj-nnelirr  15851  triap  15930