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  2823  vtocl3gf  2824  vtoclegft  2833  sbcthdv  3001  disji2  4023  exmid1stab  4238  swopolem  4337  funssres  5297  fvmptssdm  5643  fmptcof  5726  fliftfuns  5842  isorel  5852  oveqrspc2v  5946  caovclg  6073  caovcomg  6076  caovassg  6079  caovcang  6082  caovordig  6086  caovordg  6088  caovdig  6095  caovdirg  6098  qliftfuns  6675  nneneq  6915  supmoti  7054  exmidonfinlem  7255  recexprlemopl  7687  recexprlemopu  7689  cauappcvgprlemladdrl  7719  caucvgsrlemcl  7851  caucvgsrlemfv  7853  caucvgsr  7864  suplocsrlempr  7869  ltordlem  8503  lble  8968  uz11  9618  seq3caopr3  10565  climcaucn  11497  sumdc  11504  fsum3  11533  fsumf1o  11536  fsum3cvg2  11540  isummulc2  11572  fsum2dlemstep  11580  fisumcom2  11584  fsumshftm  11591  fisum0diag2  11593  fsum00  11608  isumshft  11636  clim2prod  11685  prodmodclem2  11723  zproddc  11725  fprodseq  11729  fprodf1o  11734  prodssdc  11735  fprodm1s  11747  fprodp1s  11748  fprodcllemf  11759  fprodabs  11762  fprod2dlemstep  11768  fprodcom2fi  11772  dvdsprm  12278  pythagtriplem4  12409  pcmptdvds  12486  lidrididd  12968  grpidinv2  13133  ghmlin  13321  srgrz  13483  srglz  13484  ringinvnz1ne0  13548  rrgeq0i  13763  lmodlema  13791  islmodd  13792  lsslss  13880  ssnei2  14336  psmet0  14506  psmettri2  14507  cncfi  14757  dvcn  14879  dvmptfsum  14904  nninfsellemdc  15570