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 11	. 2 |- (ps -> (ph -> ch))
4	1, 3	mpd 26	1 |- (ps -> ch)

Syntax hints:   -> wi 3

This theorem is referenced by:  ax16i 1268  a16g 1274  ceqex 1882  sbcel1gv 1976  sbcel2gv 1977  opprc3 2792  limomss 3132  sotri 3435  tz6.12c 3731  tz6.12i 3732  funbrfv 3741  ndmordi 4043  unielxp 4097  oawordeulem 4178  omass 4201  ecopoprtrn 4301  xpdom2 4428  pwen 4489  php 4499  infsdomnn 4517  isfinite2 4529  unbnnt 4619  tz9.12lem1 4639  rankr1 4654  rankxplim2 4693  aceq5lem5 4719  oncard 4809  cardne 4810  unxpdom 4824  sucxpdom 4826  alephord2i 4857  cardaleph 4865  ltbtwnpq 5064  ltrpq 5065  ltexprlem4 5125  ltexprlem7 5128  ltexpri 5129  prlem936b 5134  suplem1pr 5141  suplem2pr 5142  recexsrlem 5192  mulgt0sr 5194  map2psrpr 5200  nnind 5893  nnmulclt 5897  nn0ge0t 6072  nnnegz 6093  uzindOLD 6164  qbtwnre 6224  ser1ft 6273  sqrge0 6640  cru 6675  replimt 6700  cjret 6753  absrpclt 6798  nn0absclt 6824  climfnn 7038  blf 7796  issubg 8068  nvex 8182  blocn2 8412  occl 9120  cvexchlem 10232  cdj3lem2b 10298  elghomlem2 10317  inpws1 10387  mapdiscn 10434  cnvhmpha 10448  cnvhmphb 10449  hmphsyma 10451  hmpher 10459  neifil 10478  fgsb2 10485  efilcp2 10486

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

Copyright terms: Public domain