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  1862  gencl  2795  spsbc  3001  prexg  4245  posng  4736  sosng  4737  optocl  4740  relcnvexb  5210  funimass1  5336  dmfex  5450  f1ocnvb  5521  eqfnfv2  5663  elpreima  5684  dff13  5818  f1ocnvfv  5829  f1ocnvfvb  5830  fliftfun  5846  eusvobj2  5911  mpoxopn0yelv  6306  rntpos  6324  erexb  6626  findcard2  6959  findcard2s  6960  xpfi  7002  sbthlemi3  7034  enq0tr  7520  addnqprllem  7613  addnqprulem  7614  distrlem1prl  7668  distrlem1pru  7669  recexprlem1ssl  7719  recexprlem1ssu  7720  elrealeu  7915  addcan  8225  addcan2  8226  neg11  8296  negreb  8310  mulcanapd  8707  receuap  8715  cju  9007  nn1suc  9028  nnaddcl  9029  nndivtr  9051  znegclb  9378  zaddcllempos  9382  zmulcl  9398  zeo  9450  uz11  9643  uzp1  9654  eqreznegel  9707  xneg11  9928  xnegdi  9962  modqadd1  10472  modqmul1  10488  frec2uzltd  10514  bccmpl  10865  fz1eqb  10901  eqwrd  10994  cj11  11089  rennim  11186  resqrexlemgt0  11204  efne0  11862  dvdsabseq  12031  pcfac  12546  divsfval  13032  grpinveu  13242  mulgass  13367  dvreq1  13776  unitrrg  13901  uptx  14596  hmeocnvb  14640  tgioo  14876  bj-nnbidc  15489  bj-prexg  15643  strcollnft  15716