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  6253  oav  6687  omv  6688  oeiv  6689  f1oeng  6996  mulpipq2  7686  ltrnqg  7735  genipv  7824  subval  8465  subap0  8917  xaddval  10178  fzrevral3  10441  fzoval  10482  subsq2  11009  bcval  11111  ccatws1ls  11330  swrdrlen  11353  pfxpfxid  11401  pfxcctswrd  11402  dvdsmul1  12499  dvdsmul2  12500  gcdval  12655  eucalgval2  12750  setsvalg  13242  restval  13458  xpsfval  13561  imasmnd2  13665  ismhm  13674  mhmex  13675  subsubm  13696  subsubg  13914  qusinv  13953  isghm  13960  ghminv  13967  rngrz  14090  srglmhm  14137  ringrz  14188  imasring  14208  isrhm  14303  01eq0ring  14334  restin  15041  hmeofvalg  15168  cncfval  15437  rpcxpef  15759  rpcxpneg  15772  sgmval  15851  fsumdvdsmul  15859  lgsval  15877  2lgsoddprmlem4  15985  clwwlknon  16424