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  2863  vtocl3gf  2864  vtoclegft  2875  sbcthdv  3043  disji2  4074  exmid1stab  4291  swopolem  4395  funssres  5359  fvmptssdm  5718  fmptcof  5801  fliftfuns  5921  isorel  5931  oveqrspc2v  6027  caovclg  6157  caovcomg  6160  caovassg  6163  caovcang  6166  caovordig  6170  caovordg  6172  caovdig  6179  caovdirg  6182  qliftfuns  6764  nneneq  7014  supmoti  7156  exmidonfinlem  7367  recexprlemopl  7808  recexprlemopu  7810  cauappcvgprlemladdrl  7840  caucvgsrlemcl  7972  caucvgsrlemfv  7974  caucvgsr  7985  suplocsrlempr  7990  ltordlem  8625  lble  9090  uz11  9741  seq3caopr3  10708  ccatass  11138  swrdswrd  11232  swrdccatin1  11252  swrdccatin2  11256  climcaucn  11857  sumdc  11864  fsum3  11893  fsumf1o  11896  fsum3cvg2  11900  isummulc2  11932  fsum2dlemstep  11940  fisumcom2  11944  fsumshftm  11951  fisum0diag2  11953  fsum00  11968  isumshft  11996  clim2prod  12045  prodmodclem2  12083  zproddc  12085  fprodseq  12089  fprodf1o  12094  prodssdc  12095  fprodm1s  12107  fprodp1s  12108  fprodcllemf  12119  fprodabs  12122  fprod2dlemstep  12128  fprodcom2fi  12132  dvdsprm  12654  pythagtriplem4  12786  pcmptdvds  12863  lidrididd  13410  grpidinv2  13586  ghmlin  13780  srgrz  13942  srglz  13943  ringinvnz1ne0  14007  rrgeq0i  14222  lmodlema  14250  islmodd  14251  lsslss  14339  ssnei2  14825  psmet0  14995  psmettri2  14996  cncfi  15246  dvcn  15368  dvmptfsum  15393  usgruspgrben  15978  nninfsellemdc  16335