Theorem mpan9 265

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 116	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100

This theorem is referenced by:  sylan  267  vtocl2gf  2615  vtocl3gf  2616  vtoclegft  2625  sbcthdv  2778  swopolem  4042  funssres  4942  fvmptssdm  5255  fmptcof  5331  fliftfuns  5438  isorel  5448  caovclg  5653  caovcomg  5656  caovassg  5659  caovcang  5662  caovordig  5666  caovordg  5668  caovdig  5675  caovdirg  5678  qliftfuns  6190  nneneq  6320  recexprlemopl  6723  recexprlemopu  6725  cauappcvgprlemladdrl  6755  caucvgsrlemcl  6873  caucvgsrlemfv  6875  caucvgsr  6886  uz11  8495  iseqfeq  9231  iseqcaopr3  9240  climcaucn  9870