Theorem mpd3an3 1320

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 1185	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpdan 418	1 |- ( ( ph /\ ps ) -> th )

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

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 965

This theorem is referenced by:  stoic2b  1410  elovmpo  6021  oav  6401  omv  6402  oeiv  6403  f1oeng  6702  mulpipq2  7291  ltrnqg  7340  genipv  7429  subval  8067  subap0  8518  xaddval  9749  fzrevral3  10009  fzoval  10047  subsq2  10526  bcval  10623  dvdsmul1  11709  dvdsmul2  11710  gcdval  11843  eucalgval2  11930  setsvalg  12231  restval  12368  restin  12587  hmeofvalg  12714  cncfval  12970  rpcxpef  13226  rpcxpneg  13239