let Q be Quantum_Mechanics; :: thesis: for p, q, r being Element of Prop Q st p <==> q & q <==> r holds
p <==> r
let p, q, r be Element of Prop Q; :: thesis: ( p <==> q & q <==> r implies p <==> r )
assume ( p |- q & q |- p & q |- r & r |- q ) ; :: according to QMAX_1:def 11 :: thesis: p <==> r
hence ( p |- r & r |- p ) by Th22; :: according to QMAX_1:def 11 :: thesis: verum