Theorem imbitrid 154

Description: A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.)

Hypotheses

Ref	Expression
imbitrid.1	⊢ (𝜑 → 𝜓)
imbitrid.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
imbitrid	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem imbitrid

Step	Hyp	Ref	Expression
1		imbitrid.1	. 2 ⊢ (𝜑 → 𝜓)
2		imbitrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	2	biimpd 144	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	1, 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:  syl5ibcom  155  imbitrrid  156  sbft  1896  gencl  2835  spsbc  3043  prexg  4301  posng  4798  sosng  4799  optocl  4802  relcnvexb  5276  funimass1  5407  dmfex  5526  f1ocnvb  5597  eqfnfv2  5745  elpreima  5766  dff13  5909  f1ocnvfv  5920  f1ocnvfvb  5921  fliftfun  5937  eusvobj2  6004  mpoxopn0yelv  6405  rntpos  6423  erexb  6727  findcard2  7078  findcard2s  7079  xpfi  7124  sbthlemi3  7158  enq0tr  7654  addnqprllem  7747  addnqprulem  7748  distrlem1prl  7802  distrlem1pru  7803  recexprlem1ssl  7853  recexprlem1ssu  7854  elrealeu  8049  addcan  8359  addcan2  8360  neg11  8430  negreb  8444  mulcanapd  8841  receuap  8849  cju  9141  nn1suc  9162  nnaddcl  9163  nndivtr  9185  znegclb  9512  zaddcllempos  9516  zmulcl  9533  zeo  9585  uz11  9779  uzp1  9790  eqreznegel  9848  xneg11  10069  xnegdi  10103  modqadd1  10624  modqmul1  10640  frec2uzltd  10666  bccmpl  11017  fz1eqb  11053  eqwrd  11155  ccatopth  11298  ccatopth2  11299  swrdccatin2  11311  cj11  11467  rennim  11564  resqrexlemgt0  11582  efne0  12241  dvdsabseq  12410  pcfac  12925  divsfval  13413  grpinveu  13623  mulgass  13748  dvreq1  14159  unitrrg  14284  uptx  15001  hmeocnvb  15045  tgioo  15281  uspgrf1oedg  16030  usgr0vb  16087  bj-nnbidc  16374  bj-prexg  16527  strcollnft  16600