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  7455  ltrnqg  7504  genipv  7593  subval  8235  subap0  8687  xaddval  9937  fzrevral3  10199  fzoval  10240  subsq2  10756  bcval  10858  dvdsmul1  11995  dvdsmul2  11996  gcdval  12151  eucalgval2  12246  setsvalg  12733  restval  12947  xpsfval  13050  imasmnd2  13154  ismhm  13163  mhmex  13164  subsubm  13185  subsubg  13403  qusinv  13442  isghm  13449  ghminv  13456  rngrz  13578  srglmhm  13625  ringrz  13676  imasring  13696  isrhm  13790  01eq0ring  13821  restin  14496  hmeofvalg  14623  cncfval  14892  rpcxpef  15214  rpcxpneg  15227  sgmval  15303  fsumdvdsmul  15311  lgsval  15329  2lgsoddprmlem4  15437