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	⊢ (𝜑 → 𝜓)
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 124	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

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  2783  vtocl3gf  2784  vtoclegft  2793  sbcthdv  2960  disji2  3969  swopolem  4277  funssres  5224  fvmptssdm  5564  fmptcof  5646  fliftfuns  5760  isorel  5770  caovclg  5985  caovcomg  5988  caovassg  5991  caovcang  5994  caovordig  5998  caovordg  6000  caovdig  6007  caovdirg  6010  qliftfuns  6576  nneneq  6814  supmoti  6949  exmidonfinlem  7140  recexprlemopl  7557  recexprlemopu  7559  cauappcvgprlemladdrl  7589  caucvgsrlemcl  7721  caucvgsrlemfv  7723  caucvgsr  7734  suplocsrlempr  7739  ltordlem  8371  lble  8833  uz11  9479  seq3caopr3  10406  climcaucn  11278  sumdc  11285  fsum3  11314  fsumf1o  11317  fsum3cvg2  11321  isummulc2  11353  fsum2dlemstep  11361  fisumcom2  11365  fsumshftm  11372  fisum0diag2  11374  fsum00  11389  isumshft  11417  clim2prod  11466  prodmodclem2  11504  zproddc  11506  fprodseq  11510  fprodf1o  11515  prodssdc  11516  fprodm1s  11528  fprodp1s  11529  fprodcllemf  11540  fprodabs  11543  fprod2dlemstep  11549  fprodcom2fi  11553  dvdsprm  12048  pythagtriplem4  12177  pcmptdvds  12252  ssnei2  12698  psmet0  12868  psmettri2  12869  cncfi  13106  dvcn  13205  exmid1stab  13714  nninfsellemdc  13724