Theorem mpd3an3 1372

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

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

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 1004

This theorem is referenced by:  stoic2b  1472  elovmpo  6216  oav  6617  omv  6618  oeiv  6619  f1oeng  6925  mulpipq2  7584  ltrnqg  7633  genipv  7722  subval  8364  subap0  8816  xaddval  10073  fzrevral3  10335  fzoval  10376  subsq2  10902  bcval  11004  ccatws1ls  11212  swrdrlen  11235  pfxpfxid  11283  pfxcctswrd  11284  dvdsmul1  12367  dvdsmul2  12368  gcdval  12523  eucalgval2  12618  setsvalg  13105  restval  13321  xpsfval  13424  imasmnd2  13528  ismhm  13537  mhmex  13538  subsubm  13559  subsubg  13777  qusinv  13816  isghm  13823  ghminv  13830  rngrz  13952  srglmhm  13999  ringrz  14050  imasring  14070  isrhm  14165  01eq0ring  14196  restin  14893  hmeofvalg  15020  cncfval  15289  rpcxpef  15611  rpcxpneg  15624  sgmval  15700  fsumdvdsmul  15708  lgsval  15726  2lgsoddprmlem4  15834  clwwlknon  16238