Theorem mpd3an3 1349

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

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

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 982

This theorem is referenced by:  stoic2b  1441  elovmpo  6126  oav  6521  omv  6522  oeiv  6523  f1oeng  6825  mulpipq2  7457  ltrnqg  7506  genipv  7595  subval  8237  subap0  8689  xaddval  9939  fzrevral3  10201  fzoval  10242  subsq2  10758  bcval  10860  dvdsmul1  11997  dvdsmul2  11998  gcdval  12153  eucalgval2  12248  setsvalg  12735  restval  12949  xpsfval  13052  imasmnd2  13156  ismhm  13165  mhmex  13166  subsubm  13187  subsubg  13405  qusinv  13444  isghm  13451  ghminv  13458  rngrz  13580  srglmhm  13627  ringrz  13678  imasring  13698  isrhm  13792  01eq0ring  13823  restin  14520  hmeofvalg  14647  cncfval  14916  rpcxpef  15238  rpcxpneg  15251  sgmval  15327  fsumdvdsmul  15335  lgsval  15353  2lgsoddprmlem4  15461