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  6210  oav  6608  omv  6609  oeiv  6610  f1oeng  6916  mulpipq2  7569  ltrnqg  7618  genipv  7707  subval  8349  subap0  8801  xaddval  10053  fzrevral3  10315  fzoval  10356  subsq2  10881  bcval  10983  ccatws1ls  11188  swrdrlen  11208  pfxpfxid  11256  pfxcctswrd  11257  dvdsmul1  12339  dvdsmul2  12340  gcdval  12495  eucalgval2  12590  setsvalg  13077  restval  13293  xpsfval  13396  imasmnd2  13500  ismhm  13509  mhmex  13510  subsubm  13531  subsubg  13749  qusinv  13788  isghm  13795  ghminv  13802  rngrz  13924  srglmhm  13971  ringrz  14022  imasring  14042  isrhm  14137  01eq0ring  14168  restin  14865  hmeofvalg  14992  cncfval  15261  rpcxpef  15583  rpcxpneg  15596  sgmval  15672  fsumdvdsmul  15680  lgsval  15698  2lgsoddprmlem4  15806