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  1901  gencl  2854  spsbc  3063  prexg  4347  posng  4845  sosng  4846  optocl  4849  xpexcnvm  5140  relcnvexb  5325  funimass1  5456  dmfex  5580  f1ocnvb  5651  eqfnfv2  5801  elpreima  5822  dff13  5968  f1ocnvfv  5979  f1ocnvfvb  5980  fliftfun  5996  eusvobj2  6065  mpoxopn0yelv  6504  rntpos  6522  erexb  6826  findcard2  7187  findcard2s  7188  xpfi  7233  sbthlemi3  7270  enq0tr  7795  addnqprllem  7888  addnqprulem  7889  distrlem1prl  7943  distrlem1pru  7944  recexprlem1ssl  7994  recexprlem1ssu  7995  elrealeu  8190  addcan  8500  addcan2  8501  neg11  8571  negreb  8585  mulcanapd  8983  receuap  8993  cju  9285  nn1suc  9306  nnaddcl  9307  nndivtr  9329  znegclb  9660  zaddcllempos  9664  zmulcl  9681  zeo  9734  uz11  9928  uzp1  9939  eqreznegel  9997  xneg11  10219  xnegdi  10253  modqadd1  10781  modqmul1  10797  frec2uzltd  10823  bccmpl  11175  bcm1n  11190  fz1eqb  11212  eqwrd  11328  ccatopth  11471  ccatopth2  11472  swrdccatin2  11484  cj11  11654  rennim  11751  resqrexlemgt0  11769  efne0  12428  dvdsabseq  12597  pcfac  13112  divsfval  13632  grpinveu  13826  mulgass  13945  dvreq1  14432  unitrrg  14559  uptx  15358  hmeocnvb  15402  tgioo  15638  uspgrf1oedg  16400  usgr0vb  16457  bj-nnbidc  16768  bj-prexg  16920  strcollnft  16993