Theorem mp3an 642

Description: An inference based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mp3an	|- th

Proof of Theorem mp3an

Step	Hyp	Ref	Expression
1		mp3an.2	. 2 |- ps
2		mp3an.3	. 2 |- ch
3		mp3an.1	. . 3 |- ph
4		mp3an.4	. . 3 |- ((ph /\ ps /\ ch) -> th)
5	3, 4	mp3an1 639	. 2 |- ((ps /\ ch) -> th)
6	1, 2, 5	mp2an 520	1 |- th

Syntax hints:   -> wi 2   /\ w3a 581

This theorem is referenced by:  vtocl3 1380  ordom 2382  tfrlem8 2956  ondomon 3662  1lt2pi 3826  addass 4108  mulass 4109  adddi 4110  adddir 4111  add12 4128  add23 4129  addsubass 4152  addsub 4153  mul23 4179  lttr 4307  lelttr 4308  ltletr 4309  letr 4310  ltadd2 4312  ruclem13 4897  hvmulass 5020  hvdistr1 5023  hvass 5025  hvadd23 5026  hv2times 5033  normlem0 5062  normlem9 5070  normlem8 5071  bcseq 5073  norm-ii 5086  norm-iii 5087  occllem1 5180  h1de2 5458  pjadj 5564  pjdifnorm 5574  pjcj 5575

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