Theorem mpani 434

Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Hypotheses

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

Assertion

Ref	Expression
mpani	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem mpani

Step	Hyp	Ref	Expression
1		mpani.1	. . 3 ⊢ 𝜓
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝜓)
3		mpani.2	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
4	2, 3	mpand 433	1 ⊢ (𝜑 → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mp2ani  436  mulgt1  9202  recgt1i  9237  recreclt  9239  nngt0  9339  nnrecgt0  9352  elnnnn0c  9620  elnnz1  9679  recnz  9751  uz3m2nn  9990  ledivge1le  10145  expubnd  11055  expnbnd  11123  expnlbnd  11124  sin02gt0  12557  oddge22np1  12674  dvdsnprmd  12929  prmlem1  13252  prmlem2  13264  reeff1olem  16009  sinq12gt0  16069  logdivlti  16123  gausslemma2dlem4  16400