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  4295  posng  4791  sosng  4792  optocl  4795  relcnvexb  5268  funimass1  5398  dmfex  5517  f1ocnvb  5588  eqfnfv2  5735  elpreima  5756  dff13  5898  f1ocnvfv  5909  f1ocnvfvb  5910  fliftfun  5926  eusvobj2  5993  mpoxopn0yelv  6391  rntpos  6409  erexb  6713  findcard2  7059  findcard2s  7060  xpfi  7102  sbthlemi3  7134  enq0tr  7629  addnqprllem  7722  addnqprulem  7723  distrlem1prl  7777  distrlem1pru  7778  recexprlem1ssl  7828  recexprlem1ssu  7829  elrealeu  8024  addcan  8334  addcan2  8335  neg11  8405  negreb  8419  mulcanapd  8816  receuap  8824  cju  9116  nn1suc  9137  nnaddcl  9138  nndivtr  9160  znegclb  9487  zaddcllempos  9491  zmulcl  9508  zeo  9560  uz11  9753  uzp1  9764  eqreznegel  9817  xneg11  10038  xnegdi  10072  modqadd1  10591  modqmul1  10607  frec2uzltd  10633  bccmpl  10984  fz1eqb  11020  eqwrd  11120  ccatopth  11256  ccatopth2  11257  swrdccatin2  11269  cj11  11424  rennim  11521  resqrexlemgt0  11539  efne0  12197  dvdsabseq  12366  pcfac  12881  divsfval  13369  grpinveu  13579  mulgass  13704  dvreq1  14114  unitrrg  14239  uptx  14956  hmeocnvb  15000  tgioo  15236  uspgrf1oedg  15982  bj-nnbidc  16145  bj-prexg  16298  strcollnft  16371