Theorem mpd3an3 1349

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

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

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 982

This theorem is referenced by:  stoic2b  1441  elovmpo  6117  oav  6507  omv  6508  oeiv  6509  f1oeng  6811  mulpipq2  7431  ltrnqg  7480  genipv  7569  subval  8211  subap0  8662  xaddval  9911  fzrevral3  10173  fzoval  10214  subsq2  10718  bcval  10820  dvdsmul1  11956  dvdsmul2  11957  gcdval  12096  eucalgval2  12191  setsvalg  12648  restval  12856  xpsfval  12931  ismhm  13033  mhmex  13034  subsubm  13055  subsubg  13267  qusinv  13306  isghm  13313  ghminv  13320  rngrz  13442  srglmhm  13489  ringrz  13540  imasring  13560  isrhm  13654  01eq0ring  13685  restin  14344  hmeofvalg  14471  cncfval  14727  rpcxpef  15029  rpcxpneg  15042  lgsval  15120  2lgsoddprmlem4  15200