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  6252  oav  6686  omv  6687  oeiv  6688  f1oeng  6995  mulpipq2  7682  ltrnqg  7731  genipv  7820  subval  8461  subap0  8913  xaddval  10174  fzrevral3  10437  fzoval  10478  subsq2  11005  bcval  11107  ccatws1ls  11323  swrdrlen  11346  pfxpfxid  11394  pfxcctswrd  11395  dvdsmul1  12492  dvdsmul2  12493  gcdval  12648  eucalgval2  12743  setsvalg  13231  restval  13447  xpsfval  13550  imasmnd2  13654  ismhm  13663  mhmex  13664  subsubm  13685  subsubg  13903  qusinv  13942  isghm  13949  ghminv  13956  rngrz  14079  srglmhm  14126  ringrz  14177  imasring  14197  isrhm  14292  01eq0ring  14323  restin  15028  hmeofvalg  15155  cncfval  15424  rpcxpef  15746  rpcxpneg  15759  sgmval  15838  fsumdvdsmul  15846  lgsval  15864  2lgsoddprmlem4  15972  clwwlknon  16411