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	⊢ (𝜑 → 𝜓)
mpan9.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
mpan9	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mpan9

Step	Hyp	Ref	Expression
1		mpan9.1	. . 3 ⊢ (𝜑 → 𝜓)
2		mpan9.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5 32	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 125	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

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  2834  vtocl3gf  2835  vtoclegft  2844  sbcthdv  3012  disji2  4036  exmid1stab  4251  swopolem  4351  funssres  5312  fvmptssdm  5663  fmptcof  5746  fliftfuns  5866  isorel  5876  oveqrspc2v  5970  caovclg  6098  caovcomg  6101  caovassg  6104  caovcang  6107  caovordig  6111  caovordg  6113  caovdig  6120  caovdirg  6123  qliftfuns  6705  nneneq  6953  supmoti  7094  exmidonfinlem  7300  recexprlemopl  7737  recexprlemopu  7739  cauappcvgprlemladdrl  7769  caucvgsrlemcl  7901  caucvgsrlemfv  7903  caucvgsr  7914  suplocsrlempr  7919  ltordlem  8554  lble  9019  uz11  9670  seq3caopr3  10634  ccatass  11062  climcaucn  11604  sumdc  11611  fsum3  11640  fsumf1o  11643  fsum3cvg2  11647  isummulc2  11679  fsum2dlemstep  11687  fisumcom2  11691  fsumshftm  11698  fisum0diag2  11700  fsum00  11715  isumshft  11743  clim2prod  11792  prodmodclem2  11830  zproddc  11832  fprodseq  11836  fprodf1o  11841  prodssdc  11842  fprodm1s  11854  fprodp1s  11855  fprodcllemf  11866  fprodabs  11869  fprod2dlemstep  11875  fprodcom2fi  11879  dvdsprm  12401  pythagtriplem4  12533  pcmptdvds  12610  lidrididd  13156  grpidinv2  13332  ghmlin  13526  srgrz  13688  srglz  13689  ringinvnz1ne0  13753  rrgeq0i  13968  lmodlema  13996  islmodd  13997  lsslss  14085  ssnei2  14571  psmet0  14741  psmettri2  14742  cncfi  14992  dvcn  15114  dvmptfsum  15139  nninfsellemdc  15880