Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical conjunction
mp2an
Next ⟩
mp4an
Metamath Proof Explorer
Ascii
Unicode
Theorem
mp2an
Description:
An inference based on modus ponens.
(Contributed by
NM
, 13-Apr-1995)
Ref
Expression
Hypotheses
mp2an.1
⊢
φ
mp2an.2
⊢
ψ
mp2an.3
⊢
φ
∧
ψ
→
χ
Assertion
mp2an
⊢
χ
Proof
Step
Hyp
Ref
Expression
1
mp2an.1
⊢
φ
2
mp2an.2
⊢
ψ
3
mp2an.3
⊢
φ
∧
ψ
→
χ
4
1
3
mpan
⊢
ψ
→
χ
5
2
4
ax-mp
⊢
χ