Theorem mpcom 60

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

Syntax hints:   -> wi 3

This theorem is referenced by:  ax16i 1647  ceqex 2391  sbcel1gvOLD 2511  sbcel2gvOLD 2513  opprc3 3543  limomss 3956  elimasni 4292  sotri 4315  f1ocnv 4651  tz6.12c 4697  tz6.12i 4698  funbrfv 4709  ndmordi 4984  unielxp 5047  oawordeulem 5236  omass 5259  ecopoprtrn 5370  xpdom2 5501  pwen 5597  php 5607  infsdomnn 5625  xpfi 5632  isfinite2 5639  unbnn3 5746  tz9.12lem1 5770  rankr1 5785  rankxplim2 5824  aceq5lem5 5901  oncard 5978  cardne 5980  unxpdom 5996  sucxpdom 5998  alephord2i 6025  cardaleph 6033  ltbtwnpq 6236  ltrpq 6237  ltexprlem4 6297  ltexprlem7 6300  ltexpri 6301  prlem936b 6306  suplem1pr 6313  suplem2pr 6314  recexsrlem 6364  mulgt0sr 6366  map2psrpr 6372  nnind 7120  nnmulcl 7124  nn0ge0 7326  nnnegz 7347  uzindOLD 7420  qbtwnre 7459  ser1f 7741  sqrge0i 7952  crui 7987  replim 8011  cjre 8060  absrpcl 8106  nn0abscl 8131  climfnn 8352  infpss 8843  blf 9121  issubg 9425  nvex 9562  blocn2 9808  indexfi 10174  elghomlem2 10194  cnvhmpha 10240  fillsb 10270  neifil 10302  hausfillim2 10325  opidon2 10371  isexid2 10372  grpmnd 10393  ringidmlem 10409  uznzr 10416  occli 10814  cvexchlem 11940  cdj3lem2b 12009  bnj962 12856  bnj936 13336  bnj1052 13395  bnj1125 13430  ublbneg 13653  altopth2sn 14091  inpws1 14345  fldsqcp2 14378  set2elt 14408  cmprelid2 14447  injrec 14461  surjsec 14462  repcpwti 14503  prl 14512  prl2 14514  preotr2 14576  ubos2 14598  mxlelt2 14606  mnlelt2 14608  defse3 14614  istoset2 14628  dfps2 14634  ablcomgrp 14702  clfsebs 14707  isppm 14715  gaplc 14731  grpdrcan 14738  grpdlcan 14739  rnplrnml3 14768  mulinvsca 14823  truni2 14850  truni3 14851  mapdiscnlem 14870  mapdiscn 14871  cnvhmphb 14880  hmphsyma 14882  hmpher 14890  top2usne 14898  ptincpw 14912  intcont 14914  fgsb2 14925  efilcp2 14926  fbfgss2 14937  limvinlv 14941  conttnf 14944  bwt2 14960  trhom 14983  trhom2 14985  tpgprop2 14987  cntrsetlem 14999  lvsovso 15038  lvsovso3 15040  dualcat2lem 15129  dualded2lem 15130  subctct 15202  idsubfun 15206  elincin 15220  tarax3d2 15225  tarax3f 15229  emptar 15231  tartwo 15233  tarsuc2 15245  tarsuc3 15246  intrtael 15256  valdom 15261  tartarmap 15265  vtarsuelt 15272  inttarcar 15278  carinttar 15279  fnctartar 15284  fnctartar2 15285  isseg2 15305  t1sep 15546  nrmsep2 15555  indexfiOLD 15755  iccshftri 15858  iccshftli 15860  iccdili 15862  icccntri 15864  totbndbnd 15944  pcoval 16073  pi1bval 16088  iscringd 16147  ax10ext 16364  iotavalsb 16398  smoge 16454

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

Copyright terms: Public domain