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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used by:  sylan  283  vtocl2gf  2885  vtocl3gf  2886  vtoclegft  2897  sbcthdv  3066  disji2  4122  exmid1stab  4347  swopolem  4452  funssres  5423  fvmptssdm  5793  fmptcof  5878  fliftfuns  6007  isorel  6017  oveqrspc2v  6115  caovclg  6245  caovcomg  6248  caovassg  6251  caovcang  6254  caovordig  6258  caovordg  6260  caovdig  6267  caovdirg  6270  qliftfuns  6897  nneneq  7162  supmoti  7339  exmidonfinlem  7551  recexprlemopl  7998  recexprlemopu  8000  cauappcvgprlemladdrl  8030  caucvgsrlemcl  8162  caucvgsrlemfv  8164  caucvgsr  8175  suplocsrlempr  8180  ltordlem  8817  lble  9285  uz11  9961  seq3caopr3  10949  hashfibclem  11304  ccatass  11398  swrdswrd  11499  swrdccatin1  11519  swrdccatin2  11523  climcaucn  12142  sumdc  12149  fsum3  12179  fsumf1o  12182  fsum3cvg2  12186  isummulc2  12218  fsum2dlemstep  12226  fisumcom2  12230  fsumshftm  12237  fisum0diag2  12239  fsum00  12254  isumshft  12282  clim2prod  12331  prodmodclem2  12369  zproddc  12371  fprodseq  12375  fprodf1o  12380  prodssdc  12381  fprodm1s  12393  fprodp1s  12394  fprodcllemf  12405  fprodabs  12408  fprod2dlemstep  12414  fprodcom2fi  12418  dvdsprm  12941  pythagtriplem4  13076  pcmptdvds  13153  lidrididd  13761  grpidinv2  13922  ghmlin  14110  cntzmhm2  14174  gsumsnfdcmn  14257  idjusnfi  14270  srgrz  14395  srglz  14396  ringinvnz1ne0  14461  rrgeq0i  14681  lmodlema  14737  islmodd  14738  lsslss  14827  assalem  15112  ssnei2  15383  psmet0  15553  psmettri2  15554  cncfi  15804  dvcn  15926  dvmptfsum  15951  usgruspgrben  16632  wlk1walkdom  16805  clwwlknonex2lem2  16884  nninfsellemdc  17259