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  6119  oav  6509  omv  6510  oeiv  6511  f1oeng  6813  mulpipq2  7433  ltrnqg  7482  genipv  7571  subval  8213  subap0  8664  xaddval  9914  fzrevral3  10176  fzoval  10217  subsq2  10721  bcval  10823  dvdsmul1  11959  dvdsmul2  11960  gcdval  12099  eucalgval2  12194  setsvalg  12651  restval  12859  xpsfval  12934  ismhm  13036  mhmex  13037  subsubm  13058  subsubg  13270  qusinv  13309  isghm  13316  ghminv  13323  rngrz  13445  srglmhm  13492  ringrz  13543  imasring  13563  isrhm  13657  01eq0ring  13688  restin  14355  hmeofvalg  14482  cncfval  14751  rpcxpef  15070  rpcxpneg  15083  lgsval  15161  2lgsoddprmlem4  15269