bi2bian9 Show Code edit
# Deduction joining two biconditionals with different antecedents.
## Join biconditionals
thm (bi2bian9 () (bi2an9.1 (-> ph (<-> ps ch)) bi2an9.2 (-> th (<-> ta et))) (-> (/\ ph th) (<-> (<-> ps ta) (<-> ch et))) bi2an9.1 th adantr bi2an9.2 ph adantl bibi12d)
(-> (/\ ph th) (<-> (<-> ps ta) (<-> ch et)))
edit