Theorem mpd3an3 1353

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

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

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 985

This theorem is referenced by:  stoic2b  1452  elovmpo  6175  oav  6570  omv  6571  oeiv  6572  f1oeng  6878  mulpipq2  7526  ltrnqg  7575  genipv  7664  subval  8306  subap0  8758  xaddval  10009  fzrevral3  10271  fzoval  10312  subsq2  10836  bcval  10938  ccatws1ls  11139  swrdrlen  11159  pfxpfxid  11207  pfxcctswrd  11208  dvdsmul1  12290  dvdsmul2  12291  gcdval  12446  eucalgval2  12541  setsvalg  13028  restval  13244  xpsfval  13347  imasmnd2  13451  ismhm  13460  mhmex  13461  subsubm  13482  subsubg  13700  qusinv  13739  isghm  13746  ghminv  13753  rngrz  13875  srglmhm  13922  ringrz  13973  imasring  13993  isrhm  14087  01eq0ring  14118  restin  14815  hmeofvalg  14942  cncfval  15211  rpcxpef  15533  rpcxpneg  15546  sgmval  15622  fsumdvdsmul  15630  lgsval  15648  2lgsoddprmlem4  15756