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  2751  vtocl3gf  2752  vtoclegft  2761  sbcthdv  2927  disji2  3930  swopolem  4235  funssres  5173  fvmptssdm  5513  fmptcof  5595  fliftfuns  5707  isorel  5717  caovclg  5931  caovcomg  5934  caovassg  5937  caovcang  5940  caovordig  5944  caovordg  5946  caovdig  5953  caovdirg  5956  qliftfuns  6521  nneneq  6759  supmoti  6888  exmidonfinlem  7066  recexprlemopl  7457  recexprlemopu  7459  cauappcvgprlemladdrl  7489  caucvgsrlemcl  7621  caucvgsrlemfv  7623  caucvgsr  7634  suplocsrlempr  7639  ltordlem  8268  lble  8729  uz11  9372  seq3caopr3  10285  climcaucn  11152  sumdc  11159  fsum3  11188  fsumf1o  11191  fsum3cvg2  11195  isummulc2  11227  fsum2dlemstep  11235  fisumcom2  11239  fsumshftm  11246  fisum0diag2  11248  fsum00  11263  isumshft  11291  clim2prod  11340  prodmodclem2  11378  zproddc  11380  fprodseq  11384  dvdsprm  11853  ssnei2  12365  psmet0  12535  psmettri2  12536  cncfi  12773  dvcn  12872  exmid1stab  13368  nninfsellemdc  13381