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

Theorem mpancom 413
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 403 1 (𝜓𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  mpan  415  spesbc  2913  onsucelsucr  4298  sucunielr  4300  ordsuc  4352  peano2b  4402  xpiindim  4541  fvelrnb  5315  fliftcnv  5535  riotaprop  5592  unielxp  5901  dmtpos  5975  tpossym  5995  ercnv  6265  cnvct  6478  php5dom  6531  3xpfi  6591  recrecnq  6897  1idpr  7095  eqlei2  7523  lem1  8243  eluzfz1  9377  fzpred  9414  uznfz  9447  fz0fzdiffz0  9469  fzctr  9472  flid  9619  flqeqceilz  9653  faclbnd3  10047  bcn1  10062  isfinite4im  10097  leabs  10402  gcd0id  10845  lcmgcdlem  10934  dvdsnprmd  10982  bj-nn0suc0  11283
  Copyright terms: Public domain W3C validator