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 1308  a16g 1314  ceqex 1932  sbcel1gv 2028  sbcel2gv 2029  opprc3 2873  limomss 3224  sotri 3535  tz6.12c 3851  tz6.12i 3852  funbrfv 3861  ndmordi 4112  unielxp 4167  oawordeulem 4324  omass 4347  ecopoprtrn 4452  xpdom2 4583  pwen 4650  php 4660  infsdomnn 4678  xpfi 4685  isfinite2 4692  unbnn3 4785  tz9.12lem1 4805  rankr1 4820  rankxplim2 4859  aceq5lem5 4885  oncard 4976  cardne 4978  unxpdom 4994  sucxpdom 4996  alephord2i 5027  cardaleph 5035  ltbtwnpq 5238  ltrpq 5239  ltexprlem4 5299  ltexprlem7 5302  ltexpri 5303  prlem936b 5308  suplem1pr 5315  suplem2pr 5316  recexsrlem 5366  mulgt0sr 5368  map2psrpr 5374  nnind 6082  nnmulcl 6086  nn0ge0 6285  nnnegz 6306  uzindOLD 6379  qbtwnre 6418  ser1f 6693  sqrge0i 6903  crui 6938  replim 6962  cjre 7011  absrpcl 7057  nn0abscl 7082  climfnn 7295  infpss 7786  blf 8054  issubg 8358  nvex 8477  blocn2 8723  occli 9457  cvexchlem 10576  cdj3lem2b 10646  elghomlem2 10668  inpws1 10739  domintreflem 10766  fldsqcp2 10780  set2elt 10827  opidon2 10900  isexid2 10901  isppm 10917  grpmnd 10933  rnplrnml3 10950  uridm 10956  uznzr 10967  truni2 11000  truni3 11001  mapdiscn 11014  cnvhmpha 11031  cnvhmphb 11032  hmphsyma 11034  hmpher 11042  top2usne 11051  fillsb 11073  neifil 11080  fgsb2 11086  efilcp2 11087  bwt2 11123  subctct 11308  idsubfun 11312  t1sep 11607  nrmsep2 11616  indexf 11847  iccshftri 11923  iccshftli 11925  iccdili 11927  icccntri 11929  totbndbnd 12000

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

Copyright terms: Public domain