ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpancom Structured version   GIF version

Theorem mpancom 401
Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpancom.1 (ψφ)
mpancom.2 ((φ ψ) → χ)
Assertion
Ref Expression
mpancom (ψχ)

Proof of Theorem mpancom
StepHypRef Expression
1 mpancom.1 . 2 (ψφ)
2 id 19 . 2 (ψψ)
3 mpancom.2 . 2 ((φ ψ) → χ)
41, 2, 3syl2anc 393 1 (ψχ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  mpan  402  spesbc  2820  onsucelsucr  4183  sucunielr  4185  ordsuc  4225  peano2b  4264  xpiindim  4400  fvelrnb  5146  fliftcnv  5360  riotaprop  5415  unielxp  5723  dmtpos  5793  tpossym  5813  ercnv  6038  recrecnq  6253  1idpr  6431  eqlei2  6708  bj-nn0suc0  7172
  Copyright terms: Public domain W3C validator