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  2826  vtocl3gf  2827  vtoclegft  2836  sbcthdv  3004  disji2  4027  exmid1stab  4242  swopolem  4341  funssres  5301  fvmptssdm  5647  fmptcof  5730  fliftfuns  5846  isorel  5856  oveqrspc2v  5950  caovclg  6077  caovcomg  6080  caovassg  6083  caovcang  6086  caovordig  6090  caovordg  6092  caovdig  6099  caovdirg  6102  qliftfuns  6679  nneneq  6919  supmoti  7060  exmidonfinlem  7262  recexprlemopl  7694  recexprlemopu  7696  cauappcvgprlemladdrl  7726  caucvgsrlemcl  7858  caucvgsrlemfv  7860  caucvgsr  7871  suplocsrlempr  7876  ltordlem  8511  lble  8976  uz11  9626  seq3caopr3  10585  climcaucn  11518  sumdc  11525  fsum3  11554  fsumf1o  11557  fsum3cvg2  11561  isummulc2  11593  fsum2dlemstep  11601  fisumcom2  11605  fsumshftm  11612  fisum0diag2  11614  fsum00  11629  isumshft  11657  clim2prod  11706  prodmodclem2  11744  zproddc  11746  fprodseq  11750  fprodf1o  11755  prodssdc  11756  fprodm1s  11768  fprodp1s  11769  fprodcllemf  11780  fprodabs  11783  fprod2dlemstep  11789  fprodcom2fi  11793  dvdsprm  12315  pythagtriplem4  12447  pcmptdvds  12524  lidrididd  13035  grpidinv2  13200  ghmlin  13388  srgrz  13550  srglz  13551  ringinvnz1ne0  13615  rrgeq0i  13830  lmodlema  13858  islmodd  13859  lsslss  13947  ssnei2  14403  psmet0  14573  psmettri2  14574  cncfi  14824  dvcn  14946  dvmptfsum  14971  nninfsellemdc  15664