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  2879  vtocl3gf  2880  vtoclegft  2891  sbcthdv  3059  disji2  4103  exmid1stab  4323  swopolem  4428  funssres  5397  fvmptssdm  5764  fmptcof  5846  fliftfuns  5973  isorel  5983  oveqrspc2v  6079  caovclg  6209  caovcomg  6212  caovassg  6215  caovcang  6218  caovordig  6222  caovordg  6224  caovdig  6231  caovdirg  6234  qliftfuns  6855  nneneq  7113  supmoti  7286  exmidonfinlem  7498  recexprlemopl  7942  recexprlemopu  7944  cauappcvgprlemladdrl  7974  caucvgsrlemcl  8106  caucvgsrlemfv  8108  caucvgsr  8119  suplocsrlempr  8124  ltordlem  8758  lble  9223  uz11  9880  seq3caopr3  10857  hashfibclem  11210  ccatass  11300  swrdswrd  11401  swrdccatin1  11421  swrdccatin2  11425  climcaucn  12040  sumdc  12047  fsum3  12077  fsumf1o  12080  fsum3cvg2  12084  isummulc2  12116  fsum2dlemstep  12124  fisumcom2  12128  fsumshftm  12135  fisum0diag2  12137  fsum00  12152  isumshft  12180  clim2prod  12229  prodmodclem2  12267  zproddc  12269  fprodseq  12273  fprodf1o  12278  prodssdc  12279  fprodm1s  12291  fprodp1s  12292  fprodcllemf  12303  fprodabs  12306  fprod2dlemstep  12312  fprodcom2fi  12316  dvdsprm  12838  pythagtriplem4  12970  pcmptdvds  13047  lidrididd  13612  grpidinv2  13788  ghmlin  13982  srgrz  14145  srglz  14146  ringinvnz1ne0  14210  rrgeq0i  14426  lmodlema  14457  islmodd  14458  lsslss  14546  ssnei2  15039  psmet0  15209  psmettri2  15210  cncfi  15460  dvcn  15582  dvmptfsum  15607  usgruspgrben  16198  wlk1walkdom  16371  clwwlknonex2lem2  16450  nninfsellemdc  16805