Theorem mpanr1 703

Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpanr1.1	⊢ 𝜓
mpanr1.2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
mpanr1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mpanr1

Step	Hyp	Ref	Expression
1		mpanr1.1	. 2 ⊢ 𝜓
2		mpanr1.2	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	anassrs 467	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 701	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  mpanr12  705  oacl  8460  omcl  8461  oaordi  8471  oawordri  8475  oaass  8486  oarec  8487  omordi  8491  omwordri  8497  odi  8504  omass  8505  oeoelem  8523  undom  8989  fimax2g  9191  fimin2g  9408  frr1  9674  axcnre  11077  divdiv23zi  11895  recp1lt1  12041  divgt0i  12051  divge0i  12052  ltreci  12053  lereci  12054  lt2msqi  12055  le2msqi  12056  msq11i  12057  ltdiv23i  12067  ltdivp1i  12069  zmin  12863  ge0gtmnf  13092  hashprg  14320  sqrt11i  15310  sqrtmuli  15311  sqrtmsq2i  15313  sqrtlei  15314  sqrtlti  15315  cos01gt0  16118  wspthsnwspthsnon  29879  vc2OLD  30530  vc0  30536  vcm  30538  nvpi  30629  nvge0  30635  ipval3  30671  ipidsq  30672  sspmval  30695  opsqrlem1  32102  opsqrlem6  32107  hstle  32192  hstrbi  32228  atordi  32346  weiunlem2  36439  finorwe  37358  poimirlem6  37608  poimirlem7  37609  poimirlem16  37618  poimirlem19  37621  poimirlem20  37622