nic-justbi Show Code edit
# Show equivalence between the bidirectional and the Nicod version.
# (Contributed by Jeff Hoffman, 19-Nov-2007.)
thm (nic-justbi () () (<-> (<-> ph ps) (-/\ (-/\ ph ps) (-/\ (-/\ ph ph) (-/\ ps ps)))) (/\ ph ps) (/\ (-. ph) (-. ps)) pm4.57 (-/\ ph ps) (-/\ (-/\ ph ph) (-/\ ps ps)) df-nand ph ps df-nand (-/\ ph ph) (-/\ ps ps) df-nand ph nic-justneg ps nic-justneg anbi12i notbii bitr4i anbi12i notbii bitri ph ps dfbi3 3bitr4ri)
(<-> (<-> ph ps) (-/\ (-/\ ph ps) (-/\ (-/\ ph ph) (-/\ ps ps))))
edit