Theorem mpancom 769

Description: An inference based on modus ponens with commutation of antecedents.

Hypotheses

Ref	Expression
mpancom.1	|- (ps -> ph)
mpancom.2	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
mpancom	|- (ps -> ch)

Proof of Theorem mpancom

Step	Hyp	Ref	Expression
1		mpancom.1	. 2 |- (ps -> ph)
2		mpancom.2	. . 3 |- ((ph /\ ps) -> ch)
3	2	ancoms 484	. 2 |- ((ps /\ ph) -> ch)
4	1, 3	mpdan 768	1 |- (ps -> ch)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  reuuni3 3812  orduniorsuc 3909  dffv2 4734  unielxp 5047  fodomfi 5656  pwfilem 5660  cardnn 5870  ondomcard 6009  ltexprlem4 6297  ledivp1i 7089  ltdivp1i 7090  flid 7474  eluzfz 7647  seqzcl 7801  crre 8019  crim 8020  faclbnd3 8199  faclbnd4lem4 8203  bcxmaslem1 8334  caucvg3lem 8426  eftlubcl 8638  issubgi 9431  ablmul 9439  isga 9450  isga2 9452  gaid 9454  ssga 9455  vcoprnelem 9529  htthlem9 9975  symggrpi 10205  usinuniop 10341  ismgm 10367  ismnd2 10392  unmnd 10405  fora 10408  on1el3 10412  on1el4 10413  hilabl 10660  mayete3i 11308  mayete3OLDi 11309  homulid2 11363  lnopeqi 11570  cnlnadjlem7 11643  adjbdlnb 11654  nmopcoadji 11671  bracnlnval 11685  hmopidmchlem 11722  hmopidmchi 11723  hmopidmpji 11724  gcd0id 13729  alalifal 14327  islatalg 14531  isprs 14565  gaplc 14731  topgrpi 14972  mamb 15030  obsubc2 15198  idsubc 15199  domsubc 15200  codsubc 15201  cmpsubc 15204  filnetlem4 15643  filnet 15645  fsumlt1 15831  icoopnst 15876  atombase 17003

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

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain