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  9194  recgt1i  9229  recreclt  9231  nngt0  9330  nnrecgt0  9343  elnnnn0c  9610  elnnz1  9669  recnz  9741  uz3m2nn  9975  ledivge1le  10129  expubnd  11035  expnbnd  11103  expnlbnd  11104  sin02gt0  12533  oddge22np1  12650  dvdsnprmd  12905  reeff1olem  15874  sinq12gt0  15934  logdivlti  15986  gausslemma2dlem4  16195