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 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

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

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 1011

This theorem is referenced by:  stoic2b  1479  elovmpo  6282  oav  6721  omv  6722  oeiv  6723  f1oeng  7037  mulpipq2  7732  ltrnqg  7781  genipv  7870  subval  8512  subap0  8965  xaddval  10230  fzrevral3  10497  fzoval  10538  subsq2  11067  bcval  11170  ccatws1ls  11393  swrdrlen  11416  pfxpfxid  11464  pfxcctswrd  11465  dvdsmul1  12563  dvdsmul2  12564  gcdval  12719  eucalgval2  12814  setsvalg  13365  restval  13582  xpsfval  13652  imasmnd2  13742  ismhm  13751  mhmex  13752  subsubm  13773  subsubg  13983  qusinv  14022  isghm  14029  ghminv  14036  rngrz  14228  srglmhm  14280  ringrz  14332  imasring  14352  isrhm  14448  01eq0ring  14479  restin  15260  hmeofvalg  15387  cncfval  15656  rpcxpef  15979  rpcxpneg  15992  sgmval  16080  fsumdvdsmul  16088  lgsval  16106  2lgsoddprmlem4  16214  clwwlknon  16653