Theorem mpanr1 700

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 468	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 698	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  mpanr12  702  oacl  8365  omcl  8366  oaordi  8377  oawordri  8381  oaass  8392  oarec  8393  omordi  8397  omwordri  8403  odi  8410  omass  8411  oeoelem  8429  undom  8846  fimax2g  9060  fimin2g  9256  frr1  9517  axcnre  10920  divdiv23zi  11728  recp1lt1  11873  divgt0i  11883  divge0i  11884  ltreci  11885  lereci  11886  lt2msqi  11887  le2msqi  11888  msq11i  11889  ltdiv23i  11899  ltdivp1i  11901  zmin  12684  ge0gtmnf  12906  hashprg  14110  sqrt11i  15096  sqrtmuli  15097  sqrtmsq2i  15099  sqrtlei  15100  sqrtlti  15101  cos01gt0  15900  wspthsnwspthsnon  28281  vc2OLD  28930  vc0  28936  vcm  28938  nvpi  29029  nvge0  29035  ipval3  29071  ipidsq  29072  sspmval  29095  opsqrlem1  30502  opsqrlem6  30507  hstle  30592  hstrbi  30628  atordi  30746  finorwe  35553  poimirlem6  35783  poimirlem7  35784  poimirlem16  35793  poimirlem19  35796  poimirlem20  35797