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  6732  omv  6733  oeiv  6734  f1oeng  7049  mulpipq2  7744  ltrnqg  7793  genipv  7882  subval  8525  subap0  8979  xaddval  10263  fzrevral3  10530  fzoval  10571  subsq2  11104  bcval  11208  ccatws1ls  11431  swrdrlen  11454  pfxpfxid  11502  pfxcctswrd  11503  dvdsmul1  12604  dvdsmul2  12605  gcdval  12760  eucalgval2  12855  setsvalg  13439  restval  13657  xpsfval  13727  imasmnd2  13817  ismhm  13826  mhmex  13827  subsubm  13848  subsubg  14058  qusinv  14097  isghm  14104  ghminv  14111  rngrz  14351  srglmhm  14403  ringrz  14455  imasring  14477  isrhm  14573  01eq0ring  14604  restin  15419  hmeofvalg  15546  cncfval  15815  rpcxpef  16144  rpcxpneg  16157  sgmval  16269  fsumdvdsmul  16302  lgsval  16345  2lgsoddprmlem4  16453  clwwlknon  16892