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  6291  oav  6731  omv  6732  oeiv  6733  f1oeng  7047  mulpipq2  7744  ltrnqg  7793  genipv  7882  subval  8525  subap0  8979  xaddval  10264  fzrevral3  10531  fzoval  10572  subsq2  11105  bcval  11209  ccatws1ls  11432  swrdrlen  11455  pfxpfxid  11503  pfxcctswrd  11504  dvdsmul1  12605  dvdsmul2  12606  gcdval  12761  eucalgval2  12856  setsvalg  13440  restval  13658  xpsfval  13728  imasmnd2  13818  ismhm  13827  mhmex  13828  subsubm  13849  subsubg  14059  qusinv  14098  isghm  14105  ghminv  14112  rngrz  14352  srglmhm  14404  ringrz  14456  imasring  14478  isrhm  14574  01eq0ring  14605  restin  15402  hmeofvalg  15529  cncfval  15798  rpcxpef  16127  rpcxpneg  16140  sgmval  16252  fsumdvdsmul  16285  lgsval  16328  2lgsoddprmlem4  16436  clwwlknon  16875