Theorem mpd3an3 1375

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

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

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 1007

This theorem is referenced by:  stoic2b  1475  elovmpo  6255  oav  6689  omv  6690  oeiv  6691  f1oeng  6998  mulpipq2  7691  ltrnqg  7740  genipv  7829  subval  8470  subap0  8922  xaddval  10184  fzrevral3  10448  fzoval  10489  subsq2  11016  bcval  11119  ccatws1ls  11338  swrdrlen  11361  pfxpfxid  11409  pfxcctswrd  11410  dvdsmul1  12507  dvdsmul2  12508  gcdval  12663  eucalgval2  12758  setsvalg  13263  restval  13479  xpsfval  13582  imasmnd2  13686  ismhm  13695  mhmex  13696  subsubm  13717  subsubg  13935  qusinv  13974  isghm  13981  ghminv  13988  rngrz  14111  srglmhm  14158  ringrz  14209  imasring  14229  isrhm  14325  01eq0ring  14356  restin  15090  hmeofvalg  15217  cncfval  15486  rpcxpef  15808  rpcxpneg  15821  sgmval  15900  fsumdvdsmul  15908  lgsval  15926  2lgsoddprmlem4  16034  clwwlknon  16473