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  2801  vtocl3gf  2802  vtoclegft  2811  sbcthdv  2979  disji2  3998  exmid1stab  4210  swopolem  4307  funssres  5260  fvmptssdm  5602  fmptcof  5685  fliftfuns  5801  isorel  5811  oveqrspc2v  5904  caovclg  6029  caovcomg  6032  caovassg  6035  caovcang  6038  caovordig  6042  caovordg  6044  caovdig  6051  caovdirg  6054  qliftfuns  6621  nneneq  6859  supmoti  6994  exmidonfinlem  7194  recexprlemopl  7626  recexprlemopu  7628  cauappcvgprlemladdrl  7658  caucvgsrlemcl  7790  caucvgsrlemfv  7792  caucvgsr  7803  suplocsrlempr  7808  ltordlem  8441  lble  8906  uz11  9552  seq3caopr3  10483  climcaucn  11361  sumdc  11368  fsum3  11397  fsumf1o  11400  fsum3cvg2  11404  isummulc2  11436  fsum2dlemstep  11444  fisumcom2  11448  fsumshftm  11455  fisum0diag2  11457  fsum00  11472  isumshft  11500  clim2prod  11549  prodmodclem2  11587  zproddc  11589  fprodseq  11593  fprodf1o  11598  prodssdc  11599  fprodm1s  11611  fprodp1s  11612  fprodcllemf  11623  fprodabs  11626  fprod2dlemstep  11632  fprodcom2fi  11636  dvdsprm  12139  pythagtriplem4  12270  pcmptdvds  12345  lidrididd  12806  grpidinv2  12933  srgrz  13172  srglz  13173  ringinvnz1ne0  13231  lmodlema  13387  islmodd  13388  lsslss  13473  ssnei2  13696  psmet0  13866  psmettri2  13867  cncfi  14104  dvcn  14203  nninfsellemdc  14798