Description: Part (6) of Baer p. 47 line 6. Note that we use
-. X e. ( N{ Y , Z } ) which is equivalent to Baer's "Fx i^i
(Fy + Fz)" by lspdisjb . TODO: If disjoint variable conditions with
I and ph become a problem later, use cbv* theorems on I
variables here to get rid of them. Maybe reorder hypotheses in lemmas
to the more consistent order of this theorem, so they can be shared with
this theorem. TODO: may be deleted (with its lemmas), if not needed, in
view of hdmap1l6 . (Contributed by NM, 1-May-2015)(New usage is discouraged.)