Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Abbreviated conjunction and disjunction of three wff's
3ad2antl3
Next ⟩
3ad2antr1
Metamath Proof Explorer
Ascii
Unicode
Theorem
3ad2antl3
Description:
Deduction adding conjuncts to antecedent.
(Contributed by
NM
, 4-Aug-2007)
Ref
Expression
Hypothesis
3ad2antl.1
⊢
φ
∧
χ
→
θ
Assertion
3ad2antl3
⊢
ψ
∧
τ
∧
φ
∧
χ
→
θ
Proof
Step
Hyp
Ref
Expression
1
3ad2antl.1
⊢
φ
∧
χ
→
θ
2
1
adantll
⊢
τ
∧
φ
∧
χ
→
θ
3
2
3adantl1
⊢
ψ
∧
τ
∧
φ
∧
χ
→
θ