Theorem mpd3an3 1351

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

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

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 983

This theorem is referenced by:  stoic2b  1450  elovmpo  6163  oav  6558  omv  6559  oeiv  6560  f1oeng  6866  mulpipq2  7514  ltrnqg  7563  genipv  7652  subval  8294  subap0  8746  xaddval  9997  fzrevral3  10259  fzoval  10300  subsq2  10824  bcval  10926  ccatws1ls  11127  swrdrlen  11147  pfxpfxid  11195  pfxcctswrd  11196  dvdsmul1  12209  dvdsmul2  12210  gcdval  12365  eucalgval2  12460  setsvalg  12947  restval  13162  xpsfval  13265  imasmnd2  13369  ismhm  13378  mhmex  13379  subsubm  13400  subsubg  13618  qusinv  13657  isghm  13664  ghminv  13671  rngrz  13793  srglmhm  13840  ringrz  13891  imasring  13911  isrhm  14005  01eq0ring  14036  restin  14733  hmeofvalg  14860  cncfval  15129  rpcxpef  15451  rpcxpneg  15464  sgmval  15540  fsumdvdsmul  15548  lgsval  15566  2lgsoddprmlem4  15674