Theorem mpd3an3 1374

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

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

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 1006

This theorem is referenced by:  stoic2b  1474  elovmpo  6226  oav  6627  omv  6628  oeiv  6629  f1oeng  6935  mulpipq2  7596  ltrnqg  7645  genipv  7734  subval  8376  subap0  8828  xaddval  10085  fzrevral3  10347  fzoval  10388  subsq2  10915  bcval  11017  ccatws1ls  11228  swrdrlen  11251  pfxpfxid  11299  pfxcctswrd  11300  dvdsmul1  12397  dvdsmul2  12398  gcdval  12553  eucalgval2  12648  setsvalg  13135  restval  13351  xpsfval  13454  imasmnd2  13558  ismhm  13567  mhmex  13568  subsubm  13589  subsubg  13807  qusinv  13846  isghm  13853  ghminv  13860  rngrz  13983  srglmhm  14030  ringrz  14081  imasring  14101  isrhm  14196  01eq0ring  14227  restin  14929  hmeofvalg  15056  cncfval  15325  rpcxpef  15647  rpcxpneg  15660  sgmval  15736  fsumdvdsmul  15744  lgsval  15762  2lgsoddprmlem4  15870  clwwlknon  16309