Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical equivalence
syl5ibcom
Next ⟩
imbitrrid
Metamath Proof Explorer
Ascii
Unicode
Theorem
syl5ibcom
Description:
A mixed syllogism inference.
(Contributed by
NM
, 19-Jun-2007)
Ref
Expression
Hypotheses
imbitrid.1
⊢
φ
→
ψ
imbitrid.2
⊢
χ
→
ψ
↔
θ
Assertion
syl5ibcom
⊢
φ
→
χ
→
θ
Proof
Step
Hyp
Ref
Expression
1
imbitrid.1
⊢
φ
→
ψ
2
imbitrid.2
⊢
χ
→
ψ
↔
θ
3
1
2
imbitrid
⊢
χ
→
φ
→
θ
4
3
com12
⊢
φ
→
χ
→
θ