Theorem mpd3an3 1379

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  stoic2b  1479  elovmpo  6291  oav  6731  omv  6732  oeiv  6733  f1oeng  7048  mulpipq2  7745  ltrnqg  7794  genipv  7883  subval  8526  subap0  8980  xaddval  10265  fzrevral3  10532  fzoval  10573  subsq2  11106  bcval  11210  ccatws1ls  11433  swrdrlen  11456  pfxpfxid  11504  pfxcctswrd  11505  dvdsmul1  12606  dvdsmul2  12607  gcdval  12762  eucalgval2  12857  setsvalg  13441  restval  13659  xpsfval  13729  imasmnd2  13819  ismhm  13828  mhmex  13829  subsubm  13850  subsubg  14060  qusinv  14099  isghm  14106  ghminv  14113  rngrz  14353  srglmhm  14405  ringrz  14457  imasring  14479  isrhm  14575  01eq0ring  14606  restin  15414  hmeofvalg  15541  cncfval  15810  rpcxpef  16139  rpcxpneg  16152  sgmval  16264  fsumdvdsmul  16297  lgsval  16340  2lgsoddprmlem4  16448  clwwlknon  16887