Theorem mpd3an3 1349

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

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

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 982

This theorem is referenced by:  stoic2b  1441  elovmpo  6122  oav  6512  omv  6513  oeiv  6514  f1oeng  6816  mulpipq2  7438  ltrnqg  7487  genipv  7576  subval  8218  subap0  8670  xaddval  9920  fzrevral3  10182  fzoval  10223  subsq2  10739  bcval  10841  dvdsmul1  11978  dvdsmul2  11979  gcdval  12126  eucalgval2  12221  setsvalg  12708  restval  12916  xpsfval  12991  ismhm  13093  mhmex  13094  subsubm  13115  subsubg  13327  qusinv  13366  isghm  13373  ghminv  13380  rngrz  13502  srglmhm  13549  ringrz  13600  imasring  13620  isrhm  13714  01eq0ring  13745  restin  14412  hmeofvalg  14539  cncfval  14808  rpcxpef  15130  rpcxpneg  15143  sgmval  15219  fsumdvdsmul  15227  lgsval  15245  2lgsoddprmlem4  15353