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  1894  gencl  2832  spsbc  3040  prexg  4296  posng  4793  sosng  4794  optocl  4797  relcnvexb  5271  funimass1  5401  dmfex  5520  f1ocnvb  5591  eqfnfv2  5738  elpreima  5759  dff13  5901  f1ocnvfv  5912  f1ocnvfvb  5913  fliftfun  5929  eusvobj2  5996  mpoxopn0yelv  6396  rntpos  6414  erexb  6718  findcard2  7064  findcard2s  7065  xpfi  7110  sbthlemi3  7142  enq0tr  7637  addnqprllem  7730  addnqprulem  7731  distrlem1prl  7785  distrlem1pru  7786  recexprlem1ssl  7836  recexprlem1ssu  7837  elrealeu  8032  addcan  8342  addcan2  8343  neg11  8413  negreb  8427  mulcanapd  8824  receuap  8832  cju  9124  nn1suc  9145  nnaddcl  9146  nndivtr  9168  znegclb  9495  zaddcllempos  9499  zmulcl  9516  zeo  9568  uz11  9762  uzp1  9773  eqreznegel  9826  xneg11  10047  xnegdi  10081  modqadd1  10600  modqmul1  10616  frec2uzltd  10642  bccmpl  10993  fz1eqb  11029  eqwrd  11130  ccatopth  11269  ccatopth2  11270  swrdccatin2  11282  cj11  11437  rennim  11534  resqrexlemgt0  11552  efne0  12210  dvdsabseq  12379  pcfac  12894  divsfval  13382  grpinveu  13592  mulgass  13717  dvreq1  14127  unitrrg  14252  uptx  14969  hmeocnvb  15013  tgioo  15249  uspgrf1oedg  15995  usgr0vb  16052  bj-nnbidc  16230  bj-prexg  16383  strcollnft  16456