Theorem mpd3an3 1372

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

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

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 1004

This theorem is referenced by:  stoic2b  1472  elovmpo  6203  oav  6598  omv  6599  oeiv  6600  f1oeng  6906  mulpipq2  7554  ltrnqg  7603  genipv  7692  subval  8334  subap0  8786  xaddval  10037  fzrevral3  10299  fzoval  10340  subsq2  10864  bcval  10966  ccatws1ls  11168  swrdrlen  11188  pfxpfxid  11236  pfxcctswrd  11237  dvdsmul1  12319  dvdsmul2  12320  gcdval  12475  eucalgval2  12570  setsvalg  13057  restval  13273  xpsfval  13376  imasmnd2  13480  ismhm  13489  mhmex  13490  subsubm  13511  subsubg  13729  qusinv  13768  isghm  13775  ghminv  13782  rngrz  13904  srglmhm  13951  ringrz  14002  imasring  14022  isrhm  14116  01eq0ring  14147  restin  14844  hmeofvalg  14971  cncfval  15240  rpcxpef  15562  rpcxpneg  15575  sgmval  15651  fsumdvdsmul  15659  lgsval  15677  2lgsoddprmlem4  15785