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  6288  oav  6727  omv  6728  oeiv  6729  f1oeng  7043  mulpipq2  7738  ltrnqg  7787  genipv  7876  subval  8518  subap0  8972  xaddval  10249  fzrevral3  10516  fzoval  10557  subsq2  11086  bcval  11189  ccatws1ls  11412  swrdrlen  11435  pfxpfxid  11483  pfxcctswrd  11484  dvdsmul1  12582  dvdsmul2  12583  gcdval  12738  eucalgval2  12833  setsvalg  13384  restval  13601  xpsfval  13671  imasmnd2  13761  ismhm  13770  mhmex  13771  subsubm  13792  subsubg  14002  qusinv  14041  isghm  14048  ghminv  14055  rngrz  14247  srglmhm  14299  ringrz  14351  imasring  14371  isrhm  14467  01eq0ring  14498  restin  15279  hmeofvalg  15406  cncfval  15675  rpcxpef  16002  rpcxpneg  16015  sgmval  16103  fsumdvdsmul  16111  lgsval  16135  2lgsoddprmlem4  16243  clwwlknon  16682