Theorem mpan9 281

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  sylan  283  vtocl2gf  2822  vtocl3gf  2823  vtoclegft  2832  sbcthdv  3000  disji2  4022  exmid1stab  4237  swopolem  4336  funssres  5296  fvmptssdm  5642  fmptcof  5725  fliftfuns  5841  isorel  5851  oveqrspc2v  5945  caovclg  6071  caovcomg  6074  caovassg  6077  caovcang  6080  caovordig  6084  caovordg  6086  caovdig  6093  caovdirg  6096  qliftfuns  6673  nneneq  6913  supmoti  7052  exmidonfinlem  7253  recexprlemopl  7685  recexprlemopu  7687  cauappcvgprlemladdrl  7717  caucvgsrlemcl  7849  caucvgsrlemfv  7851  caucvgsr  7862  suplocsrlempr  7867  ltordlem  8501  lble  8966  uz11  9615  seq3caopr3  10562  climcaucn  11494  sumdc  11501  fsum3  11530  fsumf1o  11533  fsum3cvg2  11537  isummulc2  11569  fsum2dlemstep  11577  fisumcom2  11581  fsumshftm  11588  fisum0diag2  11590  fsum00  11605  isumshft  11633  clim2prod  11682  prodmodclem2  11720  zproddc  11722  fprodseq  11726  fprodf1o  11731  prodssdc  11732  fprodm1s  11744  fprodp1s  11745  fprodcllemf  11756  fprodabs  11759  fprod2dlemstep  11765  fprodcom2fi  11769  dvdsprm  12275  pythagtriplem4  12406  pcmptdvds  12483  lidrididd  12965  grpidinv2  13130  ghmlin  13318  srgrz  13480  srglz  13481  ringinvnz1ne0  13545  rrgeq0i  13760  lmodlema  13788  islmodd  13789  lsslss  13877  ssnei2  14325  psmet0  14495  psmettri2  14496  cncfi  14733  dvcn  14849  nninfsellemdc  15500