Theorem mpcom 49

Description: Modus ponens inference with commutation of antecedents.

Hypotheses

Ref	Expression
mpcom.1	|- (ps -> ph)
mpcom.2	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
mpcom	|- (ps -> ch)

Proof of Theorem mpcom

Step	Hyp	Ref	Expression
1		mpcom.1	. 2 |- (ps -> ph)
2		mpcom.2	. . 3 |- (ph -> (ps -> ch))
3	2	com12 13	. 2 |- (ps -> (ph -> ch))
4	1, 3	mpd 46	1 |- (ps -> ch)

Syntax hints:   -> wi 2

This theorem is referenced by:  a16g 933  ceqex 1410  sbcel1 1466  sbcel2 1467  opprc3 1908  limsuc 2361  limomss 2378  sotri 2630  tz6.12c 2846  tz6.12i 2847  funbrfv 2852  tfrlem9 2957  tfrlem10 2958  ndmordi 3065  oawordeulem 3156  ecopoprtrn 3247  php 3409  infsdomnn 3426  isfinite2 3437  tz9.12lem1 3503  rankr1 3518  aceq5lem5 3562  oncard 3636  cardne 3637  unxpdom 3650  sucxpdom 3652  alephord2i 3682  cardaleph 3690  ltbtwnpq 3878  ltrpq 3879  ltexprlem4 3939  ltexprlem7 3942  ltexpri 3943  prlem936b 3948  suplem1pr 3955  suplem2pr 3956  recexsrlem 4006  mulgt0sr 4008  map2psrpr 4014  nnind 4434  nnmulclt 4437  cru 4529  nn0ge0t 4550  nnnegz 4566  uzind 4603  qbtwnre 4650  sqrge0 4760  replimt 4798  cjret 4829  occl 5188  pjrn 5587  cvexchlem 5759

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

metamath.org