Theorem mpbird 171

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

Hypotheses

Ref	Expression
mpbird.min	|- (ph -> ch)
mpbird.maj	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
mpbird	|- (ph -> ps)

Proof of Theorem mpbird

Step	Hyp	Ref	Expression
1		mpbird.min	. 2 |- (ph -> ch)
2		mpbird.maj	. . 3 |- (ph -> (ps <-> ch))
3	2	biimprd 136	. 2 |- (ph -> (ch -> ps))
4	1, 3	mpd 46	1 |- (ph -> ps)

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  eqeltrd 1163  eqsstrd 1534  eqbrtrd 2077  supmo 2156  ordelon 2222  onin 2229  0ellim 2285  elelsuc 2295  onmindif 2312  onmindif2 2313  suceloni 2314  ordtri2or 2328  ssnlim 2407  relssdv 2482  iss 2599  funssres 2698  fn0 2739  fssxp 2761  fcoi1 2765  fcoi2 2766  fnopabfv 2858  fvco 2865  fsn 2895  fconst2 2902  funfvima3 2906  tfrlem11 2959  tfrlem12 2960  tfr3 2964  tz7.48-2 2995  oalim 3135  omlim 3136  oelim 3137  oen0 3165  enrefg 3294  pw2en 3348  mapenlem2 3385  mapxpen 3390  onomeneq 3414  r1ord 3499  ac6lem 3575  oncard 3636  canth3 3656  ondomcard 3663  carduni 3664  cardcf 3706  recrecpq 3867  ltaddpq 3873  genpn0 3900  ltsopr 3930  prlem934b 3932  ltaddpr 3934  reclem3pr 3952  1idsr 4001  ssgt0sr 4011  divdivdivt 4265  suprub 4513  nnunb 4520  nn0ge0t 4550  zltp1let 4597  uzwo2 4606  nn0ind 4612  zmax 4618  flleltt 4625  flidt 4627  expcllem 4682  discrlem3 4715  sqrlem12 4742  ruclem24 4908  znnen 4930  hiidrclt 5053  hiidge0t 5056  ocsh 5164  occllem6 5185  projlem1 5193  projlem2 5194  projlem12 5204  projlem25 5217  projlem26 5218  omlsilem 5249  pjopt 5264  pjpot 5265  pjoml 5271  h1did 5456  osumlem3 5532  osumlem7 5536  5oalem1 5544  5oalem2 5545  3oalem2 5553  pjot 5561  sto2 5678  stle 5681  stles 5682  atcvat3 5774

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