Theorem mpd3an3 1379

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  stoic2b  1479  elovmpo  6288  oav  6727  omv  6728  oeiv  6729  f1oeng  7043  mulpipq2  7739  ltrnqg  7788  genipv  7877  subval  8520  subap0  8974  xaddval  10258  fzrevral3  10525  fzoval  10566  subsq2  11099  bcval  11203  ccatws1ls  11426  swrdrlen  11449  pfxpfxid  11497  pfxcctswrd  11498  dvdsmul1  12599  dvdsmul2  12600  gcdval  12755  eucalgval2  12850  setsvalg  13434  restval  13652  xpsfval  13722  imasmnd2  13812  ismhm  13821  mhmex  13822  subsubm  13843  subsubg  14053  qusinv  14092  isghm  14099  ghminv  14106  rngrz  14329  srglmhm  14381  ringrz  14433  imasring  14453  isrhm  14549  01eq0ring  14580  restin  15368  hmeofvalg  15495  cncfval  15764  rpcxpef  16091  rpcxpneg  16104  sgmval  16213  fsumdvdsmul  16246  lgsval  16289  2lgsoddprmlem4  16397  clwwlknon  16836