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  893  3jao  1338  19.33b2  1678  sbequ2  1817  sbi1v  1940  mor  2122  2euex  2167  eqneqall  2413  necon3ad  2445  necon1aidc  2454  necon4addc  2473  elnelall  2510  spcimgft  2883  spcimegft  2885  rspc  2905  rspcimdv  2912  rspc2gv  2923  euind  2994  2reuswapdc  3011  reuind  3012  sbciegft  3063  rspsbc  3116  preqr2g  3855  prel12  3859  intss1  3948  intmin  3953  iinss  4027  disjiun  4088  trel3  4200  trin  4202  repizf2  4258  exmidsssnc  4299  copsexg  4342  po3nr  4413  sowlin  4423  eusvnfb  4557  reusv3  4563  ssorduni  4591  ordsucim  4604  tfis2f  4688  ssrelrel  4832  relop  4886  iss  5065  poirr2  5136  funopg  5367  funssres  5376  funun  5378  funcnvuni  5406  fv3  5671  fvmptt  5747  dff4im  5801  f1eqcocnv  5942  oprabid  6060  f1o2ndf1  6402  poxp  6406  reldmtpos  6462  rntpos  6466  smoiun  6510  tfrlem1  6517  tfrlemi1  6541  tfrexlem  6543  tfri3  6576  nntri3or  6704  qsss  6806  th3qlem1  6849  ixpsnf1o  6948  modom  7037  phplem4  7084  fimax2gtri  7134  fiintim  7166  fisseneq  7170  sbthlemi10  7208  supmoti  7235  suplub2ti  7243  ordiso2  7277  ltmpig  7602  prcdnql  7747  prcunqu  7748  recexprlem1ssl  7896  recexprlem1ssu  7897  recexprlemss1l  7898  recexprlemss1u  7899  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemladdrl  7941  mulgt0sr  8041  suplocsrlem  8071  axprecex  8143  ltxrlt  8287  addid0  8594  negf1o  8603  cju  9183  nngt1ne1  9220  nnsub  9224  0mnnnnn0  9476  un0addcl  9477  un0mulcl  9478  zapne  9598  eluzuzle  9808  indstr  9871  elpq  9927  xposdif  10161  ixxdisj  10182  icodisj  10271  uzsubsubfz  10327  elfzmlbp  10412  fzofzim  10473  subfzo0  10534  addmodlteq  10706  seq3f1olemp  10823  seqf1og  10829  expcl2lemap  10859  expnegzap  10881  expaddzap  10891  expmulzap  10893  facwordi  11048  bccl  11075  hashfacen  11146  fundm2domnop0  11158  wrdind  11352  wrd2ind  11353  swrdccatin1  11355  swrdccatin2  11359  pfxccat3  11364  pfxccat3a  11368  swrdccat3blem  11369  reuccatpfxs1  11377  ovshftex  11442  cau3lem  11737  maxabslemval  11831  rexanre  11843  xrmaxiflemval  11873  2clim  11924  summodc  12007  fsum2dlemstep  12058  fsumiun  12101  prodmodc  12202  fprod2dlemstep  12246  odd2np1lem  12496  oddge22np1  12505  sqoddm1div8z  12510  divalglemeunn  12545  divalglemeuneg  12547  bitsfzo  12579  gcd0id  12613  divgcdcoprm0  12736  prmdvdsexpr  12785  prmfac1  12787  qnumdencl  12822  hashdvds  12856  prm23lt5  12899  pcneg  12961  prmpwdvds  12991  ctinf  13114  imasaddfnlemg  13460  mnd1id  13602  0subm  13630  insubm  13631  dfgrp3mlem  13744  ringrng  14113  domnmuln0  14352  lss1d  14462  islidlm  14558  rnglidlmcl  14559  tgcl  14858  epttop  14884  txbas  15052  txbasval  15061  txcnp  15065  txdis1cn  15072  bldisj  15195  reopnap  15340  dvfgg  15482  lgsdir2lem2  15831  gausslemma2dlem1a  15860  gausslemma2dlem3  15865  gausslemma2d  15871  2lgsoddprmlem2  15908  ushgredgedg  16150  ushgredgedgloop  16152  uhgr0v0e  16158  subumgredg2en  16195  uhgrspansubgrlem  16200  wlk1walkdom  16283  upgriswlkdc  16284  uspgr2wlkeq  16289  clwwlknonex2e  16364  bj-vtoclgft  16476  bj-charfun  16506  bj-charfunbi  16510  bj-indind  16631  bj-nntrans  16650  bj-nnelirr  16652  triap  16744  gfsumval  16792