Theorem mp3an3 641

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mp3an3.1	|- ch
mp3an3.2	|- ((ph /\ ps /\ ch) -> th)

Assertion

Ref	Expression
mp3an3	|- ((ph /\ ps) -> th)

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 |- ch
2		mp3an3.2	. . 3 |- ((ph /\ ps /\ ch) -> th)
3	2	3expa 612	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	1, 3	mpan2 519	1 |- ((ph /\ ps) -> th)

Syntax hints:   -> wi 2   /\ wa 196   /\ w3a 581

This theorem is referenced by:  oprabval 3047  oprabvali 3049  oprabval2 3051  elrnoprab 3054  oaword1 3154  mapxpen 3390  unfilem1 3438  prlem934b 3932  addcan 4120  mulcan 4207  divneq0bt 4230  nnaddclt 4436  nnmulclt 4437  nnge1t 4439  nnltp1let 4449  nn0leltp1t 4557  nn0ltlem1 4558  elnnz1 4581  zleltp1t 4598  zneo 4601  uzind 4603  qbtwnre 4650  seqlem2 4663  expaddt 4698  discrlem3 4715  nneo 4719  sqrlem6 4736  sqrlem12 4742  ruclem13 4897  znnen 4930  projlem28 5220  pjthlem7 5231  spanunsn 5482  h1datom 5483  chrelat 5757  chrelat2 5758  atcvatlem 5770  atcvat3 5774

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583

metamath.org