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 ⊢ (𝜒 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  syl5ibcom  155  imbitrrid  156  sbft  1901  gencl  2854  spsbc  3063  prexg  4351  posng  4849  sosng  4850  optocl  4853  xpexcnvm  5145  relcnvexb  5330  funimass1  5461  dmfex  5585  f1ocnvb  5656  eqfnfv2  5810  elpreima  5831  dff13  5977  f1ocnvfv  5988  f1ocnvfvb  5989  fliftfun  6005  eusvobj2  6074  mpoxopn0yelv  6514  rntpos  6532  erexb  6836  findcard2  7198  findcard2s  7199  xpfi  7244  sbthlemi3  7282  enq0tr  7808  addnqprllem  7901  addnqprulem  7902  distrlem1prl  7956  distrlem1pru  7957  recexprlem1ssl  8007  recexprlem1ssu  8008  elrealeu  8203  addcan  8514  addcan2  8515  neg11  8585  negreb  8599  mulcanapd  8998  receuap  9008  cju  9300  nn1suc  9333  nnaddcl  9334  nndivtr  9356  znegclb  9689  zaddcllempos  9693  zmulcl  9710  zeo  9763  uz11  9962  uzp1  9973  eqreznegel  10031  xneg11  10254  xnegdi  10288  modqadd1  10820  modqmul1  10836  frec2uzltd  10862  bccmpl  11215  bcm1n  11230  fz1eqb  11252  eqwrd  11368  ccatopth  11511  ccatopth2  11512  swrdccatin2  11524  cj11  11694  rennim  11791  resqrexlemgt0  11809  efne0  12471  dvdsabseq  12640  pcfac  13159  divsfval  13709  grpinveu  13903  mulgass  14022  dvreq1  14559  unitrrg  14686  uptx  15512  hmeocnvb  15556  tgioo  15792  uspgrf1oedg  16634  usgr0vb  16691  bj-nnbidc  17002  bj-prexg  17154  strcollnft  17227