Theorem mpd3an3 1374

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

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

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 1006

This theorem is referenced by:  stoic2b  1474  elovmpo  6221  oav  6622  omv  6623  oeiv  6624  f1oeng  6930  mulpipq2  7591  ltrnqg  7640  genipv  7729  subval  8371  subap0  8823  xaddval  10080  fzrevral3  10342  fzoval  10383  subsq2  10910  bcval  11012  ccatws1ls  11223  swrdrlen  11246  pfxpfxid  11294  pfxcctswrd  11295  dvdsmul1  12392  dvdsmul2  12393  gcdval  12548  eucalgval2  12643  setsvalg  13130  restval  13346  xpsfval  13449  imasmnd2  13553  ismhm  13562  mhmex  13563  subsubm  13584  subsubg  13802  qusinv  13841  isghm  13848  ghminv  13855  rngrz  13978  srglmhm  14025  ringrz  14076  imasring  14096  isrhm  14191  01eq0ring  14222  restin  14919  hmeofvalg  15046  cncfval  15315  rpcxpef  15637  rpcxpneg  15650  sgmval  15726  fsumdvdsmul  15734  lgsval  15752  2lgsoddprmlem4  15860  clwwlknon  16299