Theorem mpan9 455

Description: Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpan9.1	|- (ph -> ps)
mpan9.2	|- (ch -> (ps -> th))

Assertion

Ref	Expression
mpan9	|- ((ph /\ ch) -> th)

Proof of Theorem mpan9

Step	Hyp	Ref	Expression
1		mpan9.1	. . 3 |- (ph -> ps)
2		mpan9.2	. . 3 |- (ch -> (ps -> th))
3	1, 2	syl5 28	. 2 |- (ch -> (ph -> th))
4	3	impcom 419	1 |- ((ph /\ ch) -> th)

Syntax hints:   -> wi 4   /\ wa 358

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

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  sylan  457  vtocl2gf  2917  vtocl3gf  2918  vtoclegft  2927  sbcthdv  3062  nnsucelr  4429  nnadjoin  4521  sfintfin  4533  funiunfv  5468  isorel  5490  caovcld  5623  caovcomg  5625  caovassg  5627  caovdig  5633  caovdirg  5634