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  6288  oav  6727  omv  6728  oeiv  6729  f1oeng  7043  mulpipq2  7738  ltrnqg  7787  genipv  7876  subval  8518  subap0  8971  xaddval  10247  fzrevral3  10514  fzoval  10555  subsq2  11084  bcval  11187  ccatws1ls  11410  swrdrlen  11433  pfxpfxid  11481  pfxcctswrd  11482  dvdsmul1  12580  dvdsmul2  12581  gcdval  12736  eucalgval2  12831  setsvalg  13382  restval  13599  xpsfval  13669  imasmnd2  13759  ismhm  13768  mhmex  13769  subsubm  13790  subsubg  14000  qusinv  14039  isghm  14046  ghminv  14053  rngrz  14245  srglmhm  14297  ringrz  14349  imasring  14369  isrhm  14465  01eq0ring  14496  restin  15277  hmeofvalg  15404  cncfval  15673  rpcxpef  15996  rpcxpneg  16009  sgmval  16097  fsumdvdsmul  16105  lgsval  16123  2lgsoddprmlem4  16231  clwwlknon  16670