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  6216  oav  6617  omv  6618  oeiv  6619  f1oeng  6925  mulpipq2  7581  ltrnqg  7630  genipv  7719  subval  8361  subap0  8813  xaddval  10070  fzrevral3  10332  fzoval  10373  subsq2  10899  bcval  11001  ccatws1ls  11209  swrdrlen  11232  pfxpfxid  11280  pfxcctswrd  11281  dvdsmul1  12364  dvdsmul2  12365  gcdval  12520  eucalgval2  12615  setsvalg  13102  restval  13318  xpsfval  13421  imasmnd2  13525  ismhm  13534  mhmex  13535  subsubm  13556  subsubg  13774  qusinv  13813  isghm  13820  ghminv  13827  rngrz  13949  srglmhm  13996  ringrz  14047  imasring  14067  isrhm  14162  01eq0ring  14193  restin  14890  hmeofvalg  15017  cncfval  15286  rpcxpef  15608  rpcxpneg  15621  sgmval  15697  fsumdvdsmul  15705  lgsval  15723  2lgsoddprmlem4  15831  clwwlknon  16224