Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Abbreviated conjunction and disjunction of three wff's
3adant3r2
Next ⟩
3adant3r3
Metamath Proof Explorer
Ascii
Unicode
Theorem
3adant3r2
Description:
Deduction adding a conjunct to antecedent.
(Contributed by
NM
, 17-Feb-2008)
Ref
Expression
Hypothesis
ad4ant3.1
⊢
φ
∧
ψ
∧
χ
→
θ
Assertion
3adant3r2
⊢
φ
∧
ψ
∧
τ
∧
χ
→
θ
Proof
Step
Hyp
Ref
Expression
1
ad4ant3.1
⊢
φ
∧
ψ
∧
χ
→
θ
2
1
3expb
⊢
φ
∧
ψ
∧
χ
→
θ
3
2
3adantr2
⊢
φ
∧
ψ
∧
τ
∧
χ
→
θ