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  6213  oav  6613  omv  6614  oeiv  6615  f1oeng  6921  mulpipq2  7574  ltrnqg  7623  genipv  7712  subval  8354  subap0  8806  xaddval  10058  fzrevral3  10320  fzoval  10361  subsq2  10886  bcval  10988  ccatws1ls  11194  swrdrlen  11214  pfxpfxid  11262  pfxcctswrd  11263  dvdsmul1  12345  dvdsmul2  12346  gcdval  12501  eucalgval2  12596  setsvalg  13083  restval  13299  xpsfval  13402  imasmnd2  13506  ismhm  13515  mhmex  13516  subsubm  13537  subsubg  13755  qusinv  13794  isghm  13801  ghminv  13808  rngrz  13930  srglmhm  13977  ringrz  14028  imasring  14048  isrhm  14143  01eq0ring  14174  restin  14871  hmeofvalg  14998  cncfval  15267  rpcxpef  15589  rpcxpneg  15602  sgmval  15678  fsumdvdsmul  15686  lgsval  15704  2lgsoddprmlem4  15812