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  2801  vtocl3gf  2802  vtoclegft  2811  sbcthdv  2979  disji2  3998  exmid1stab  4210  swopolem  4307  funssres  5260  fvmptssdm  5603  fmptcof  5686  fliftfuns  5802  isorel  5812  oveqrspc2v  5905  caovclg  6030  caovcomg  6033  caovassg  6036  caovcang  6039  caovordig  6043  caovordg  6045  caovdig  6052  caovdirg  6055  qliftfuns  6622  nneneq  6860  supmoti  6995  exmidonfinlem  7195  recexprlemopl  7627  recexprlemopu  7629  cauappcvgprlemladdrl  7659  caucvgsrlemcl  7791  caucvgsrlemfv  7793  caucvgsr  7804  suplocsrlempr  7809  ltordlem  8442  lble  8907  uz11  9553  seq3caopr3  10484  climcaucn  11362  sumdc  11369  fsum3  11398  fsumf1o  11401  fsum3cvg2  11405  isummulc2  11437  fsum2dlemstep  11445  fisumcom2  11449  fsumshftm  11456  fisum0diag2  11458  fsum00  11473  isumshft  11501  clim2prod  11550  prodmodclem2  11588  zproddc  11590  fprodseq  11594  fprodf1o  11599  prodssdc  11600  fprodm1s  11612  fprodp1s  11613  fprodcllemf  11624  fprodabs  11627  fprod2dlemstep  11633  fprodcom2fi  11637  dvdsprm  12140  pythagtriplem4  12271  pcmptdvds  12346  lidrididd  12808  grpidinv2  12935  srgrz  13178  srglz  13179  ringinvnz1ne0  13237  lmodlema  13393  islmodd  13394  lsslss  13479  ssnei2  13818  psmet0  13988  psmettri2  13989  cncfi  14226  dvcn  14325  nninfsellemdc  14921