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