Theorem mpd3an3 1338

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  stoic2b  1430  elovmpo  6075  oav  6458  omv  6459  oeiv  6460  f1oeng  6760  mulpipq2  7373  ltrnqg  7422  genipv  7511  subval  8152  subap0  8603  xaddval  9848  fzrevral3  10110  fzoval  10151  subsq2  10631  bcval  10732  dvdsmul1  11823  dvdsmul2  11824  gcdval  11963  eucalgval2  12056  setsvalg  12495  restval  12700  xpsfval  12774  ismhm  12860  subsubg  13067  srglmhm  13187  ringrz  13234  01eq0ring  13341  restin  13837  hmeofvalg  13964  cncfval  14220  rpcxpef  14476  rpcxpneg  14489  lgsval  14566  2lgsoddprmlem4  14621