Theorem mpd3an3 1333

Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)

Hypotheses

Ref	Expression
mpd3an3.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
mpd3an3.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mpd3an3	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mpd3an3

Step	Hyp	Ref	Expression
1		mpd3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2		mpd3an3.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expa 1198	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpdan 419	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  stoic2b  1423  elovmpo  6050  oav  6433  omv  6434  oeiv  6435  f1oeng  6735  mulpipq2  7333  ltrnqg  7382  genipv  7471  subval  8111  subap0  8562  xaddval  9802  fzrevral3  10063  fzoval  10104  subsq2  10583  bcval  10683  dvdsmul1  11775  dvdsmul2  11776  gcdval  11914  eucalgval2  12007  setsvalg  12446  restval  12585  ismhm  12685  restin  12970  hmeofvalg  13097  cncfval  13353  rpcxpef  13609  rpcxpneg  13622  lgsval  13699