Theorem mpancom 707

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

Hypotheses

Ref	Expression
mpancom.1	⊢ (ψ → φ)
mpancom.2	⊢ ((φ ⋀ ψ) → χ)

Assertion

Ref	Expression
mpancom	⊢ (ψ → χ)

Proof of Theorem mpancom

Step	Hyp	Ref	Expression
1		mpancom.1	. 2 ⊢ (ψ → φ)
2		mpancom.2	. . 3 ⊢ ((φ ⋀ ψ) → χ)
3	2	ancoms 438	. 2 ⊢ ((ψ ⋀ φ) → χ)
4	1, 3	mpdan 706	1 ⊢ (ψ → χ)

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  reuuni3 2892  orduniorsuc 3093  unielxp 4113  fodomfi 4575  fodomfiOLD 4576  pwfilem 4577  pwfilemOLD 4578  cardnn 4834  ondomcard 4868  ltexprlem4 5157  ledivp1 5908  ltdivp1 5909  flidt 6237  eluzfzt 6478  seqzcl 6559  crret 6770  crimt 6771  faclbnd3 6947  faclbnd4lem4 6951  bcxmaslem1 7074  caucvg3lem 7166  eftlubclt 7376  issubgi 8118  ablmul 8127  vcoprnelem 8193  htthlem9 8624  hilabl 9022  mayete3 9668  homulid2t 9721  lnopeq 9928  cnlnadjlem7 10001  adjbdlnb 10012  nmopcoadj 10029  bracnlnvalt 10042  hmopidmchlem 10073  hmopidmch 10074  hmopidmpj 10075  symggrpi 10401

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