Theorem mpd3an3 1351

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

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

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 983

This theorem is referenced by:  stoic2b  1450  elovmpo  6152  oav  6547  omv  6548  oeiv  6549  f1oeng  6855  mulpipq2  7491  ltrnqg  7540  genipv  7629  subval  8271  subap0  8723  xaddval  9974  fzrevral3  10236  fzoval  10277  subsq2  10799  bcval  10901  ccatws1ls  11102  swrdrlen  11122  pfxpfxid  11168  dvdsmul1  12168  dvdsmul2  12169  gcdval  12324  eucalgval2  12419  setsvalg  12906  restval  13121  xpsfval  13224  imasmnd2  13328  ismhm  13337  mhmex  13338  subsubm  13359  subsubg  13577  qusinv  13616  isghm  13623  ghminv  13630  rngrz  13752  srglmhm  13799  ringrz  13850  imasring  13870  isrhm  13964  01eq0ring  13995  restin  14692  hmeofvalg  14819  cncfval  15088  rpcxpef  15410  rpcxpneg  15423  sgmval  15499  fsumdvdsmul  15507  lgsval  15525  2lgsoddprmlem4  15633