Theorem mpancom 703

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 702	1 |- (ps -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  reuuni3 2876  orduniorsuc 3077  unielxp 4091  fodomfi 4540  pwfilem 4544  cardnn 4796  ondomcard 4829  ltexprlem4 5117  ledivp1 5854  ltdivp1 5855  flidt 6180  eluzfzt 6409  seqzcl 6490  crret 6702  crretOLD 6703  crimt 6704  crimtOLD 6705  faclbnd3 6884  faclbnd4lem4 6888  bcxmaslem1 7012  caucvg3lem 7102  eftlubclt 7318  issubgi 8059  ablmul 8068  vcoprnelem 8135  htthlem9 8558  circgrpOLD 8658  hilabl 8948  mayete3 9590  homulid2t 9643  lnopeq 9848  cnlnadjlem7 9921  adjbdlnb 9932  nmopcoadj 9948  hmopidmchlem 9989  hmopidmch 9990  hmopidmpj 9991  symggrpiOLD 10311  symggrpi 10313

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