Theorem mpd3an3 1372

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

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

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 1004

This theorem is referenced by:  stoic2b  1472  elovmpo  6210  oav  6608  omv  6609  oeiv  6610  f1oeng  6916  mulpipq2  7566  ltrnqg  7615  genipv  7704  subval  8346  subap0  8798  xaddval  10049  fzrevral3  10311  fzoval  10352  subsq2  10877  bcval  10979  ccatws1ls  11181  swrdrlen  11201  pfxpfxid  11249  pfxcctswrd  11250  dvdsmul1  12332  dvdsmul2  12333  gcdval  12488  eucalgval2  12583  setsvalg  13070  restval  13286  xpsfval  13389  imasmnd2  13493  ismhm  13502  mhmex  13503  subsubm  13524  subsubg  13742  qusinv  13781  isghm  13788  ghminv  13795  rngrz  13917  srglmhm  13964  ringrz  14015  imasring  14035  isrhm  14130  01eq0ring  14161  restin  14858  hmeofvalg  14985  cncfval  15254  rpcxpef  15576  rpcxpneg  15589  sgmval  15665  fsumdvdsmul  15673  lgsval  15691  2lgsoddprmlem4  15799