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  2837  vtocl3gf  2838  vtoclegft  2849  sbcthdv  3017  disji2  4043  exmid1stab  4260  swopolem  4360  funssres  5322  fvmptssdm  5677  fmptcof  5760  fliftfuns  5880  isorel  5890  oveqrspc2v  5984  caovclg  6112  caovcomg  6115  caovassg  6118  caovcang  6121  caovordig  6125  caovordg  6127  caovdig  6134  caovdirg  6137  qliftfuns  6719  nneneq  6969  supmoti  7110  exmidonfinlem  7317  recexprlemopl  7758  recexprlemopu  7760  cauappcvgprlemladdrl  7790  caucvgsrlemcl  7922  caucvgsrlemfv  7924  caucvgsr  7935  suplocsrlempr  7940  ltordlem  8575  lble  9040  uz11  9691  seq3caopr3  10658  ccatass  11087  swrdswrd  11181  climcaucn  11737  sumdc  11744  fsum3  11773  fsumf1o  11776  fsum3cvg2  11780  isummulc2  11812  fsum2dlemstep  11820  fisumcom2  11824  fsumshftm  11831  fisum0diag2  11833  fsum00  11848  isumshft  11876  clim2prod  11925  prodmodclem2  11963  zproddc  11965  fprodseq  11969  fprodf1o  11974  prodssdc  11975  fprodm1s  11987  fprodp1s  11988  fprodcllemf  11999  fprodabs  12002  fprod2dlemstep  12008  fprodcom2fi  12012  dvdsprm  12534  pythagtriplem4  12666  pcmptdvds  12743  lidrididd  13289  grpidinv2  13465  ghmlin  13659  srgrz  13821  srglz  13822  ringinvnz1ne0  13886  rrgeq0i  14101  lmodlema  14129  islmodd  14130  lsslss  14218  ssnei2  14704  psmet0  14874  psmettri2  14875  cncfi  15125  dvcn  15247  dvmptfsum  15272  nninfsellemdc  16088