Theorem mpbid 170

Description: A deduction from a biconditional, related to modus ponens.

Hypotheses

Ref	Expression
mpbid.min	⊢ (φ → ψ)
mpbid.maj	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
mpbid	⊢ (φ → χ)

Proof of Theorem mpbid

Step	Hyp	Ref	Expression
1		mpbid.min	. 2 ⊢ (φ → ψ)
2		mpbid.maj	. . 3 ⊢ (φ → (ψ ↔ χ))
3	2	biimpd 135	. 2 ⊢ (φ → (ψ → χ))
4	1, 3	mpd 46	1 ⊢ (φ → χ)

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  eqtrd 1128  eleqtrd 1165  eueq2 1429  eueq3 1430  zfrepclf 1477  sseqtrd 1536  3sstr3d 1542  reuhyp 1581  breqtrd 2081  3brtr3d 2086  supsn 2168  ordtri3or 2230  onint0 2262  onnmin 2270  onmindif2 2313  limsssuc 2362  dflim3 2368  finds 2397  tfindsg2 2403  feu 2767  fopab2 2891  fsn2 2896  tfrlem2 2950  tfrlem8 2956  oaass 3163  mapsn 3269  en2d 3303  mapenlem2 3385  xpmapenlem5 3395  phplem5 3407  php3 3411  php4 3412  unfilem1 3438  fiint 3445  rankr1 3518  r1rankid 3537  rankr1id 3539  aceq3 3556  cardnn 3631  cardaleph 3690  cardalephex 3691  axrepnd 3740  ltexprlem7 3942  nnind 4434  nn1suc 4435  nnleltp1t 4448  nnaddm1clt 4452  nnreclt 4522  nn0ltp1let 4556  elnnz1 4581  zaddclt 4590  zltp1let 4597  nn0ind 4612  zmax 4618  zbtwnre 4619  rebtwnz 4620  flidt 4627  seqlem2 4663  seqrn 4673  discrlem2 4714  discrlem3 4715  sqrlem12 4742  sqrlem13 4743  infxpidmlem10 4942  alephexp2 4956  his6 5057  normpyct 5093  shorth 5176  projlem8 5200  projlem13 5205  projlem26 5218  pjthlem10 5234  pjthlem11 5235  choc1 5292  osumlem3 5532  5oalem3 5546  stles 5682  stadd 5687  stadd3 5689  strlem1 5691  strlem3a 5693  strlem5 5696  chrelat 5757  atcvatlem 5770  mdsymlem5 5780  sumdmdi 5785

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128

metamath.org