Theorem mpanr1 714

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

Syntax hints:   → wi 4   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  mpanr12  716  oacl  7476  omcl  7477  oaordi  7487  oawordri  7491  oaass  7502  oarec  7503  omordi  7507  omwordri  7513  odi  7520  omass  7521  oeoelem  7539  fimax2g  8065  fimin2g  8260  axcnre  9838  divdiv23zi  10624  recp1lt1  10767  divgt0i  10778  divge0i  10779  ltreci  10780  lereci  10781  lt2msqi  10782  le2msqi  10783  msq11i  10784  ltdiv23i  10794  ltdivp1i  10796  zmin  11613  ge0gtmnf  11833  hashprg  12992  hashprgOLD  12993  sqrt11i  13915  sqrtmuli  13916  sqrtmsq2i  13918  sqrtlei  13919  sqrtlti  13920  cos01gt0  14703  0wlk  25838  0trl  25839  0pth  25863  0spth  25864  0crct  25917  0cycl  25918  0clwlk  26056  vc2OLD  26573  vc0  26587  vcm  26589  vcnegnegOLD  26592  nvnncan  26685  nvpi  26696  nvge0  26704  ipval3  26746  ipidsq  26750  sspmval  26773  opsqrlem1  28186  opsqrlem6  28191  hstle  28276  hstrbi  28312  atordi  28430  poimirlem6  32385  poimirlem7  32386  poimirlem16  32395  poimirlem19  32398  poimirlem20  32399