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  2833  spsbc  3041  prexg  4299  posng  4796  sosng  4797  optocl  4800  relcnvexb  5274  funimass1  5404  dmfex  5523  f1ocnvb  5594  eqfnfv2  5741  elpreima  5762  dff13  5904  f1ocnvfv  5915  f1ocnvfvb  5916  fliftfun  5932  eusvobj2  5999  mpoxopn0yelv  6400  rntpos  6418  erexb  6722  findcard2  7073  findcard2s  7074  xpfi  7119  sbthlemi3  7152  enq0tr  7647  addnqprllem  7740  addnqprulem  7741  distrlem1prl  7795  distrlem1pru  7796  recexprlem1ssl  7846  recexprlem1ssu  7847  elrealeu  8042  addcan  8352  addcan2  8353  neg11  8423  negreb  8437  mulcanapd  8834  receuap  8842  cju  9134  nn1suc  9155  nnaddcl  9156  nndivtr  9178  znegclb  9505  zaddcllempos  9509  zmulcl  9526  zeo  9578  uz11  9772  uzp1  9783  eqreznegel  9841  xneg11  10062  xnegdi  10096  modqadd1  10616  modqmul1  10632  frec2uzltd  10658  bccmpl  11009  fz1eqb  11045  eqwrd  11147  ccatopth  11290  ccatopth2  11291  swrdccatin2  11303  cj11  11459  rennim  11556  resqrexlemgt0  11574  efne0  12232  dvdsabseq  12401  pcfac  12916  divsfval  13404  grpinveu  13614  mulgass  13739  dvreq1  14149  unitrrg  14274  uptx  14991  hmeocnvb  15035  tgioo  15271  uspgrf1oedg  16020  usgr0vb  16077  bj-nnbidc  16303  bj-prexg  16456  strcollnft  16529