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  9677  recnz  9750  uz3m2nn  9989  ledivge1le  10144  expubnd  11054  expnbnd  11122  expnlbnd  11123  sin02gt0  12556  oddge22np1  12673  dvdsnprmd  12928  prmlem1  13251  prmlem2  13263  reeff1olem  16030  sinq12gt0  16090  logdivlti  16144  gausslemma2dlem4  16421