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  4345  swopolem  4450  funssres  5420  fvmptssdm  5790  fmptcof  5875  fliftfuns  6004  isorel  6014  oveqrspc2v  6112  caovclg  6242  caovcomg  6245  caovassg  6248  caovcang  6251  caovordig  6255  caovordg  6257  caovdig  6264  caovdirg  6267  qliftfuns  6893  nneneq  7158  supmoti  7334  exmidonfinlem  7546  recexprlemopl  7993  recexprlemopu  7995  cauappcvgprlemladdrl  8025  caucvgsrlemcl  8157  caucvgsrlemfv  8159  caucvgsr  8170  suplocsrlempr  8175  ltordlem  8812  lble  9280  uz11  9955  seq3caopr3  10943  hashfibclem  11298  ccatass  11392  swrdswrd  11493  swrdccatin1  11513  swrdccatin2  11517  climcaucn  12136  sumdc  12143  fsum3  12173  fsumf1o  12176  fsum3cvg2  12180  isummulc2  12212  fsum2dlemstep  12220  fisumcom2  12224  fsumshftm  12231  fisum0diag2  12233  fsum00  12248  isumshft  12276  clim2prod  12325  prodmodclem2  12363  zproddc  12365  fprodseq  12369  fprodf1o  12374  prodssdc  12375  fprodm1s  12387  fprodp1s  12388  fprodcllemf  12399  fprodabs  12402  fprod2dlemstep  12408  fprodcom2fi  12412  dvdsprm  12935  pythagtriplem4  13070  pcmptdvds  13147  lidrididd  13755  grpidinv2  13916  ghmlin  14104  cntzmhm2  14168  srgrz  14372  srglz  14373  ringinvnz1ne0  14438  rrgeq0i  14656  lmodlema  14712  islmodd  14713  lsslss  14802  assalem  15087  ssnei2  15349  psmet0  15519  psmettri2  15520  cncfi  15770  dvcn  15892  dvmptfsum  15917  usgruspgrben  16593  wlk1walkdom  16766  clwwlknonex2lem2  16845  nninfsellemdc  17219