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 )

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

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 1011

This theorem is referenced by:  stoic2b  1479  elovmpo  6278  oav  6717  omv  6718  oeiv  6719  f1oeng  7033  mulpipq2  7728  ltrnqg  7777  genipv  7866  subval  8508  subap0  8961  xaddval  10226  fzrevral3  10492  fzoval  10533  subsq2  11062  bcval  11165  ccatws1ls  11388  swrdrlen  11411  pfxpfxid  11459  pfxcctswrd  11460  dvdsmul1  12558  dvdsmul2  12559  gcdval  12714  eucalgval2  12809  setsvalg  13360  restval  13576  xpsfval  13646  imasmnd2  13736  ismhm  13745  mhmex  13746  subsubm  13767  subsubg  13977  qusinv  14016  isghm  14023  ghminv  14030  rngrz  14220  srglmhm  14271  ringrz  14322  imasring  14342  isrhm  14438  01eq0ring  14469  restin  15200  hmeofvalg  15327  cncfval  15596  rpcxpef  15919  rpcxpneg  15932  sgmval  16011  fsumdvdsmul  16019  lgsval  16037  2lgsoddprmlem4  16145  clwwlknon  16584