Theorem mpd3an3 1316

Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)

Hypotheses

Ref	Expression
mpd3an3.2	|- ( ( ph /\ ps ) -> ch )
mpd3an3.3	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

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

Proof of Theorem mpd3an3

Step	Hyp	Ref	Expression
1		mpd3an3.2	. 2 |- ( ( ph /\ ps ) -> ch )
2		mpd3an3.3	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expa 1181	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpdan 417	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  stoic2b  1406  elovmpo  5971  oav  6350  omv  6351  oeiv  6352  f1oeng  6651  mulpipq2  7179  ltrnqg  7228  genipv  7317  subval  7954  subap0  8405  xaddval  9628  fzrevral3  9887  fzoval  9925  subsq2  10400  bcval  10495  dvdsmul1  11515  dvdsmul2  11516  gcdval  11648  eucalgval2  11734  setsvalg  11989  restval  12126  restin  12345  hmeofvalg  12472  cncfval  12728