Theorem mpan 651

Description: An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpan.1	⊢ φ
mpan.2	⊢ ((φ ∧ ψ) → χ)

Assertion

Ref	Expression
mpan	⊢ (ψ → χ)

Proof of Theorem mpan

Step	Hyp	Ref	Expression
1		mpan.1	. . 3 ⊢ φ
2	1	a1i 10	. 2 ⊢ (ψ → φ)
3		mpan.2	. 2 ⊢ ((φ ∧ ψ) → χ)
4	2, 3	mpancom 650	1 ⊢ (ψ → χ)

Syntax hints:   → wi 4   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  mp2an  653  mpanl12  663  mp3an1  1264  mp3an12  1267  mp3an13  1268  csbex  3147  sbnfc2  3196  ssdifss  3397  uneqdifeq  3638  elssuni  3919  riinrab  4041  opkelcokg  4261  elssetkg  4269  opkelimagekg  4271  uni1exg  4292  imagekexg  4311  uniexg  4316  intexg  4319  addcexg  4393  peano5  4409  0cminle  4461  spfininduct  4540  vfinspss  4551  phiexg  4571  opexg  4587  proj1exg  4591  proj2exg  4592  copsexg  4607  imaexg  4746  siexg  4752  opeliunxp  4820  xpss2  4857  cnvexg  5101  xpexg  5114  fco  5231  fssres  5238  fvopab3g  5386  ffvelrni  5416  fvconst2  5453  oprabid  5550  caovcl  5623  caovass  5627  caovdi  5634  txpexg  5784  ins2exg  5795  imageexg  5800  txpcofun  5803  fullfunexg  5859  fvfullfun  5864  brfullfung  5865  ecelqsi  5980  ectocl  5992  pmex  6005  map0  6025  f1oen  6033  enrflxg  6034  cnven  6045  xpsnen2g  6054  enmap2lem3  6065  enmap1lem3  6071  enprmaplem5  6080  nenpw1pwlem1  6084  nulnnc  6118  ovmuc  6130  ovcelem1  6171  lec0cg  6198  sbthlem1  6203  nc0suc  6217  dflec3  6221  letc  6231  ce2t  6235  muc0or  6252  nchoicelem9  6297  nchoicelem17  6305  frecexg  6312  frecxp  6314  dmfrec  6316