Theorem mpd3an3 1375

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

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

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 1007

This theorem is referenced by:  stoic2b  1475  elovmpo  6231  oav  6665  omv  6666  oeiv  6667  f1oeng  6973  mulpipq2  7634  ltrnqg  7683  genipv  7772  subval  8413  subap0  8865  xaddval  10124  fzrevral3  10387  fzoval  10428  subsq2  10955  bcval  11057  ccatws1ls  11268  swrdrlen  11291  pfxpfxid  11339  pfxcctswrd  11340  dvdsmul1  12437  dvdsmul2  12438  gcdval  12593  eucalgval2  12688  setsvalg  13175  restval  13391  xpsfval  13494  imasmnd2  13598  ismhm  13607  mhmex  13608  subsubm  13629  subsubg  13847  qusinv  13886  isghm  13893  ghminv  13900  rngrz  14023  srglmhm  14070  ringrz  14121  imasring  14141  isrhm  14236  01eq0ring  14267  restin  14970  hmeofvalg  15097  cncfval  15366  rpcxpef  15688  rpcxpneg  15701  sgmval  15780  fsumdvdsmul  15788  lgsval  15806  2lgsoddprmlem4  15914  clwwlknon  16353