Theorem mpd3an3 1328

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

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

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 970

This theorem is referenced by:  stoic2b  1418  elovmpo  6039  oav  6422  omv  6423  oeiv  6424  f1oeng  6723  mulpipq2  7312  ltrnqg  7361  genipv  7450  subval  8090  subap0  8541  xaddval  9781  fzrevral3  10042  fzoval  10083  subsq2  10562  bcval  10662  dvdsmul1  11753  dvdsmul2  11754  gcdval  11892  eucalgval2  11985  setsvalg  12424  restval  12562  restin  12816  hmeofvalg  12943  cncfval  13199  rpcxpef  13455  rpcxpneg  13468  lgsval  13545