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  2867  vtocl3gf  2868  vtoclegft  2879  sbcthdv  3047  disji2  4085  exmid1stab  4304  swopolem  4408  funssres  5376  fvmptssdm  5740  fmptcof  5822  fliftfuns  5949  isorel  5959  oveqrspc2v  6055  caovclg  6185  caovcomg  6188  caovassg  6191  caovcang  6194  caovordig  6198  caovordg  6200  caovdig  6207  caovdirg  6210  qliftfuns  6831  nneneq  7086  supmoti  7235  exmidonfinlem  7447  recexprlemopl  7888  recexprlemopu  7890  cauappcvgprlemladdrl  7920  caucvgsrlemcl  8052  caucvgsrlemfv  8054  caucvgsr  8065  suplocsrlempr  8070  ltordlem  8704  lble  9169  uz11  9823  seq3caopr3  10799  ccatass  11234  swrdswrd  11335  swrdccatin1  11355  swrdccatin2  11359  climcaucn  11974  sumdc  11981  fsum3  12011  fsumf1o  12014  fsum3cvg2  12018  isummulc2  12050  fsum2dlemstep  12058  fisumcom2  12062  fsumshftm  12069  fisum0diag2  12071  fsum00  12086  isumshft  12114  clim2prod  12163  prodmodclem2  12201  zproddc  12203  fprodseq  12207  fprodf1o  12212  prodssdc  12213  fprodm1s  12225  fprodp1s  12226  fprodcllemf  12237  fprodabs  12240  fprod2dlemstep  12246  fprodcom2fi  12250  dvdsprm  12772  pythagtriplem4  12904  pcmptdvds  12981  lidrididd  13528  grpidinv2  13704  ghmlin  13898  srgrz  14061  srglz  14062  ringinvnz1ne0  14126  rrgeq0i  14342  lmodlema  14371  islmodd  14372  lsslss  14460  ssnei2  14951  psmet0  15121  psmettri2  15122  cncfi  15372  dvcn  15494  dvmptfsum  15519  usgruspgrben  16110  wlk1walkdom  16283  clwwlknonex2lem2  16362  nninfsellemdc  16719