Theorem mpancom 705

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 436	. 2 |- ((ps /\ ph) -> ch)
4	1, 3	mpdan 704	1 |- (ps -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  reuuni3 2886  orduniorsuc 3087  unielxp 4107  fodomfiOLD 4566  pwfilemOLD 4570  cardnn 4824  ondomcard 4857  ltexprlem4 5145  ledivp1 5906  ltdivp1 5907  flidt 6235  eluzfzt 6477  seqzcl 6558  crret 6769  crimt 6770  faclbnd3 6947  faclbnd4lem4 6951  bcxmaslem1 7074  caucvg3lem 7166  eftlubclt 7376  issubgi 8122  ablmul 8131  vcoprnelem 8197  htthlem9 8628  hilabl 9027  mayete3 9673  homulid2t 9726  lnopeq 9933  cnlnadjlem7 10006  adjbdlnb 10017  nmopcoadj 10034  bracnlnvalt 10047  hmopidmchlem 10078  hmopidmch 10079  hmopidmpj 10080  symggrpi 10406

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 147  df-an 225

Copyright terms: Public domain