Theorem mp3an1 639

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mp3an1.1	|- ph
mp3an1.2	|- ((ph /\ ps /\ ch) -> th)

Assertion

Ref	Expression
mp3an1	|- ((ps /\ ch) -> th)

Proof of Theorem mp3an1

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 |- ph
2		mp3an1.2	. . 3 |- ((ph /\ ps /\ ch) -> th)
3	2	3expb 613	. 2 |- ((ph /\ (ps /\ ch)) -> th)
4	1, 3	mpan 518	1 |- ((ps /\ ch) -> th)

Syntax hints:   -> wi 2   /\ wa 196   /\ w3a 581

This theorem is referenced by:  mp3an 642  oaord1 3153  oaword2 3155  oawordeulem 3156  oa00 3161  nnmordi 3188  unfilem2 3439  mulclpi 3815  mulidpq 3863  halfpq 3876  negeu 4124  renegcl 4171  receu 4215  ltaddpost 4363  ltplus1t 4383  nnge1t 4439  nngt0t 4441  nnrecgt0t 4447  nnaddm1clt 4452  nnunb 4520  nn0ltp1let 4556  elnn0nn 4593  qbtwnre 4650  sqr2irr 4782  znnen 4930  hvsubidt 5005  hvm1negt 5007  hvsub4t 5014  his2subt 5052  hizer1t 5054  normpyct 5093  projlem26 5218  pjsumt 5590  pjscj 5640  sto2 5678  atcveq0 5746  cvexchlem 5759  atcv0eq 5767  atcvat 5771  atcvat2 5772  atcvat3 5774  mdsymlem1 5776  sumdmd 5787

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583

metamath.org