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  1897  gencl  2845  spsbc  3053  prexg  4324  posng  4821  sosng  4822  optocl  4825  xpexcnvm  5116  relcnvexb  5301  funimass1  5432  dmfex  5556  f1ocnvb  5627  eqfnfv2  5775  elpreima  5796  dff13  5940  f1ocnvfv  5951  f1ocnvfvb  5952  fliftfun  5968  eusvobj2  6035  mpoxopn0yelv  6469  rntpos  6487  erexb  6791  findcard2  7145  findcard2s  7146  xpfi  7191  sbthlemi3  7228  enq0tr  7745  addnqprllem  7838  addnqprulem  7839  distrlem1prl  7893  distrlem1pru  7894  recexprlem1ssl  7944  recexprlem1ssu  7945  elrealeu  8140  addcan  8449  addcan2  8450  neg11  8520  negreb  8534  mulcanapd  8931  receuap  8939  cju  9231  nn1suc  9252  nnaddcl  9253  nndivtr  9275  znegclb  9606  zaddcllempos  9610  zmulcl  9627  zeo  9679  uz11  9873  uzp1  9884  eqreznegel  9942  xneg11  10163  xnegdi  10197  modqadd1  10719  modqmul1  10735  frec2uzltd  10761  bccmpl  11112  fz1eqb  11148  eqwrd  11258  ccatopth  11401  ccatopth2  11402  swrdccatin2  11414  cj11  11583  rennim  11680  resqrexlemgt0  11698  efne0  12357  dvdsabseq  12526  pcfac  13041  divsfval  13530  grpinveu  13740  mulgass  13865  dvreq1  14276  unitrrg  14402  uptx  15126  hmeocnvb  15170  tgioo  15406  uspgrf1oedg  16158  usgr0vb  16215  bj-nnbidc  16516  bj-prexg  16668  strcollnft  16741