Theorem mpd3an23 1193

Description: An inference based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mpd3an23	|- (ph -> th)

Proof of Theorem mpd3an23

Step	Hyp	Ref	Expression
1		id 73	. 2 |- (ph -> ph)
2		mpd3an23.1	. 2 |- (ph -> ps)
3		mpd3an23.2	. 2 |- (ph -> ch)
4		mpd3an23.3	. 2 |- ((ph /\ ps /\ ch) -> th)
5	1, 2, 3, 4	syl111anc 1100	1 |- (ph -> th)

Syntax hints:   -> wi 3   /\ w3a 858

This theorem is referenced by:  euuni 3807  qbtwnxr 7460  fztp 7686  grpinvid 9358  shftefif1olem 10095  chso 11224  fictblem 15370  rddif 15798  absrdbnd 15799  opoc1 16929  opoc0 16930  hl1atom 17040  grpinvidNEW 17133

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

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain