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  1872  gencl  2805  spsbc  3011  prexg  4259  posng  4751  sosng  4752  optocl  4755  relcnvexb  5227  funimass1  5356  dmfex  5472  f1ocnvb  5543  eqfnfv2  5685  elpreima  5706  dff13  5844  f1ocnvfv  5855  f1ocnvfvb  5856  fliftfun  5872  eusvobj2  5937  mpoxopn0yelv  6332  rntpos  6350  erexb  6652  findcard2  6993  findcard2s  6994  xpfi  7036  sbthlemi3  7068  enq0tr  7554  addnqprllem  7647  addnqprulem  7648  distrlem1prl  7702  distrlem1pru  7703  recexprlem1ssl  7753  recexprlem1ssu  7754  elrealeu  7949  addcan  8259  addcan2  8260  neg11  8330  negreb  8344  mulcanapd  8741  receuap  8749  cju  9041  nn1suc  9062  nnaddcl  9063  nndivtr  9085  znegclb  9412  zaddcllempos  9416  zmulcl  9433  zeo  9485  uz11  9678  uzp1  9689  eqreznegel  9742  xneg11  9963  xnegdi  9997  modqadd1  10513  modqmul1  10529  frec2uzltd  10555  bccmpl  10906  fz1eqb  10942  eqwrd  11041  cj11  11260  rennim  11357  resqrexlemgt0  11375  efne0  12033  dvdsabseq  12202  pcfac  12717  divsfval  13204  grpinveu  13414  mulgass  13539  dvreq1  13948  unitrrg  14073  uptx  14790  hmeocnvb  14834  tgioo  15070  bj-nnbidc  15767  bj-prexg  15921  strcollnft  15994