Theorem mpan9 279

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 124	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem is referenced by:  sylan  281  vtocl2gf  2792  vtocl3gf  2793  vtoclegft  2802  sbcthdv  2969  disji2  3982  swopolem  4290  funssres  5240  fvmptssdm  5580  fmptcof  5663  fliftfuns  5777  isorel  5787  oveqrspc2v  5880  caovclg  6005  caovcomg  6008  caovassg  6011  caovcang  6014  caovordig  6018  caovordg  6020  caovdig  6027  caovdirg  6030  qliftfuns  6597  nneneq  6835  supmoti  6970  exmidonfinlem  7170  recexprlemopl  7587  recexprlemopu  7589  cauappcvgprlemladdrl  7619  caucvgsrlemcl  7751  caucvgsrlemfv  7753  caucvgsr  7764  suplocsrlempr  7769  ltordlem  8401  lble  8863  uz11  9509  seq3caopr3  10437  climcaucn  11314  sumdc  11321  fsum3  11350  fsumf1o  11353  fsum3cvg2  11357  isummulc2  11389  fsum2dlemstep  11397  fisumcom2  11401  fsumshftm  11408  fisum0diag2  11410  fsum00  11425  isumshft  11453  clim2prod  11502  prodmodclem2  11540  zproddc  11542  fprodseq  11546  fprodf1o  11551  prodssdc  11552  fprodm1s  11564  fprodp1s  11565  fprodcllemf  11576  fprodabs  11579  fprod2dlemstep  11585  fprodcom2fi  11589  dvdsprm  12091  pythagtriplem4  12222  pcmptdvds  12297  lidrididd  12636  grpidinv2  12758  ssnei2  12951  psmet0  13121  psmettri2  13122  cncfi  13359  dvcn  13458  exmid1stab  14033  nninfsellemdc  14043