Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical conjunction
pm5.44
Next ⟩
pm5.42
Metamath Proof Explorer
Ascii
Unicode
Theorem
pm5.44
Description:
Theorem *5.44 of
WhiteheadRussell
p. 125.
(Contributed by
NM
, 3-Jan-2005)
Ref
Expression
Assertion
pm5.44
⊢
φ
→
ψ
→
φ
→
χ
↔
φ
→
ψ
∧
χ
Proof
Step
Hyp
Ref
Expression
1
jcab
⊢
φ
→
ψ
∧
χ
↔
φ
→
ψ
∧
φ
→
χ
2
1
baibr
⊢
φ
→
ψ
→
φ
→
χ
↔
φ
→
ψ
∧
χ