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  8574  omcl  8575  oaordi  8585  oawordri  8589  oaass  8600  oarec  8601  omordi  8605  omwordri  8611  odi  8618  omass  8619  oeoelem  8637  undom  9100  fimax2g  9323  fimin2g  9538  frr1  9800  axcnre  11205  divdiv23zi  12021  recp1lt1  12167  divgt0i  12177  divge0i  12178  ltreci  12179  lereci  12180  lt2msqi  12181  le2msqi  12182  msq11i  12183  ltdiv23i  12193  ltdivp1i  12195  zmin  12987  ge0gtmnf  13215  hashprg  14435  sqrt11i  15424  sqrtmuli  15425  sqrtmsq2i  15427  sqrtlei  15428  sqrtlti  15429  cos01gt0  16228  wspthsnwspthsnon  29937  vc2OLD  30588  vc0  30594  vcm  30596  nvpi  30687  nvge0  30693  ipval3  30729  ipidsq  30730  sspmval  30753  opsqrlem1  32160  opsqrlem6  32165  hstle  32250  hstrbi  32286  atordi  32404  weiunlem2  36465  finorwe  37384  poimirlem6  37634  poimirlem7  37635  poimirlem16  37644  poimirlem19  37647  poimirlem20  37648