Theorem mpd3an3 1375

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

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

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 1007

This theorem is referenced by:  stoic2b  1475  elovmpo  6261  oav  6700  omv  6701  oeiv  6702  f1oeng  7009  mulpipq2  7702  ltrnqg  7751  genipv  7840  subval  8482  subap0  8935  xaddval  10200  fzrevral3  10466  fzoval  10507  subsq2  11036  bcval  11139  ccatws1ls  11358  swrdrlen  11381  pfxpfxid  11429  pfxcctswrd  11430  dvdsmul1  12527  dvdsmul2  12528  gcdval  12683  eucalgval2  12778  setsvalg  13329  restval  13545  xpsfval  13615  imasmnd2  13710  ismhm  13719  mhmex  13720  subsubm  13741  subsubg  13953  qusinv  13992  isghm  13999  ghminv  14006  rngrz  14188  srglmhm  14239  ringrz  14290  imasring  14310  isrhm  14406  01eq0ring  14437  restin  15170  hmeofvalg  15297  cncfval  15566  rpcxpef  15888  rpcxpneg  15901  sgmval  15980  fsumdvdsmul  15988  lgsval  16006  2lgsoddprmlem4  16114  clwwlknon  16553