Theorem mpd3an3 1338

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  stoic2b  1430  elovmpo  6074  oav  6457  omv  6458  oeiv  6459  f1oeng  6759  mulpipq2  7372  ltrnqg  7421  genipv  7510  subval  8151  subap0  8602  xaddval  9847  fzrevral3  10109  fzoval  10150  subsq2  10630  bcval  10731  dvdsmul1  11822  dvdsmul2  11823  gcdval  11962  eucalgval2  12055  setsvalg  12494  restval  12699  xpsfval  12772  ismhm  12858  subsubg  13062  srglmhm  13181  ringrz  13228  01eq0ring  13335  restin  13761  hmeofvalg  13888  cncfval  14144  rpcxpef  14400  rpcxpneg  14413  lgsval  14490  2lgsoddprmlem4  14545