Theorem mpd3an3 1317

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 1182	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpdan 418	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

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

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 965

This theorem is referenced by:  stoic2b  1407  elovmpo  5979  oav  6358  omv  6359  oeiv  6360  f1oeng  6659  mulpipq2  7203  ltrnqg  7252  genipv  7341  subval  7978  subap0  8429  xaddval  9658  fzrevral3  9918  fzoval  9956  subsq2  10431  bcval  10527  dvdsmul1  11551  dvdsmul2  11552  gcdval  11684  eucalgval2  11770  setsvalg  12028  restval  12165  restin  12384  hmeofvalg  12511  cncfval  12767  rpcxpef  13023  rpcxpneg  13036