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  2748  vtocl3gf  2749  vtoclegft  2758  sbcthdv  2923  disji2  3922  swopolem  4227  funssres  5165  fvmptssdm  5505  fmptcof  5587  fliftfuns  5699  isorel  5709  caovclg  5923  caovcomg  5926  caovassg  5929  caovcang  5932  caovordig  5936  caovordg  5938  caovdig  5945  caovdirg  5948  qliftfuns  6513  nneneq  6751  supmoti  6880  exmidonfinlem  7049  recexprlemopl  7433  recexprlemopu  7435  cauappcvgprlemladdrl  7465  caucvgsrlemcl  7597  caucvgsrlemfv  7599  caucvgsr  7610  suplocsrlempr  7615  ltordlem  8244  lble  8705  uz11  9348  seq3caopr3  10254  climcaucn  11120  sumdc  11127  fsum3  11156  fsumf1o  11159  fsum3cvg2  11163  isummulc2  11195  fsum2dlemstep  11203  fisumcom2  11207  fsumshftm  11214  fisum0diag2  11216  fsum00  11231  isumshft  11259  clim2prod  11308  prodmodclem2  11346  dvdsprm  11817  ssnei2  12326  psmet0  12496  psmettri2  12497  cncfi  12734  dvcn  12833  exmid1stab  13195  nninfsellemdc  13206