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  2863  vtocl3gf  2864  vtoclegft  2875  sbcthdv  3043  disji2  4075  exmid1stab  4292  swopolem  4396  funssres  5360  fvmptssdm  5719  fmptcof  5802  fliftfuns  5922  isorel  5932  oveqrspc2v  6028  caovclg  6158  caovcomg  6161  caovassg  6164  caovcang  6167  caovordig  6171  caovordg  6173  caovdig  6180  caovdirg  6183  qliftfuns  6766  nneneq  7018  supmoti  7160  exmidonfinlem  7371  recexprlemopl  7812  recexprlemopu  7814  cauappcvgprlemladdrl  7844  caucvgsrlemcl  7976  caucvgsrlemfv  7978  caucvgsr  7989  suplocsrlempr  7994  ltordlem  8629  lble  9094  uz11  9745  seq3caopr3  10713  ccatass  11143  swrdswrd  11237  swrdccatin1  11257  swrdccatin2  11261  climcaucn  11862  sumdc  11869  fsum3  11898  fsumf1o  11901  fsum3cvg2  11905  isummulc2  11937  fsum2dlemstep  11945  fisumcom2  11949  fsumshftm  11956  fisum0diag2  11958  fsum00  11973  isumshft  12001  clim2prod  12050  prodmodclem2  12088  zproddc  12090  fprodseq  12094  fprodf1o  12099  prodssdc  12100  fprodm1s  12112  fprodp1s  12113  fprodcllemf  12124  fprodabs  12127  fprod2dlemstep  12133  fprodcom2fi  12137  dvdsprm  12659  pythagtriplem4  12791  pcmptdvds  12868  lidrididd  13415  grpidinv2  13591  ghmlin  13785  srgrz  13947  srglz  13948  ringinvnz1ne0  14012  rrgeq0i  14228  lmodlema  14256  islmodd  14257  lsslss  14345  ssnei2  14831  psmet0  15001  psmettri2  15002  cncfi  15252  dvcn  15374  dvmptfsum  15399  usgruspgrben  15984  wlk1walkdom  16070  nninfsellemdc  16376