Theorem mpan9 277

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 32	. 2 |- ( ch -> ( ph -> th ) )
4	3	impcom 124	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  sylan  279  vtocl2gf  2703  vtocl3gf  2704  vtoclegft  2713  sbcthdv  2876  disji2  3868  swopolem  4165  funssres  5101  fvmptssdm  5437  fmptcof  5519  fliftfuns  5631  isorel  5641  caovclg  5855  caovcomg  5858  caovassg  5861  caovcang  5864  caovordig  5868  caovordg  5870  caovdig  5877  caovdirg  5880  qliftfuns  6443  nneneq  6680  supmoti  6795  recexprlemopl  7334  recexprlemopu  7336  cauappcvgprlemladdrl  7366  caucvgsrlemcl  7484  caucvgsrlemfv  7486  caucvgsr  7497  ltordlem  8111  lble  8563  uz11  9198  seq3caopr3  10095  climcaucn  10959  sumdc  10966  fsum3  10995  fsumf1o  10998  fsum3cvg2  11002  isummulc2  11034  fsum2dlemstep  11042  fisumcom2  11046  fsumshftm  11053  fisum0diag2  11055  fsum00  11070  isumshft  11098  dvdsprm  11610  ssnei2  12108  psmet0  12255  psmettri2  12256  cncfi  12478  nninfsellemdc  12790