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