imdi - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > imdi		Unicode version

Theorem imdi 363

Description: Distributive law for implication. Compare Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.)

**Assertion**
Ref	Expression
imdi

**Proof of Theorem imdi**
Step	Hyp	Ref	Expression
1		ax-2 7	. 2
2		pm2.86 100	. 2
3	1, 2	impbii 188	1

Colors of variables: wff setvar class

Syntax hints: ->wi 4 <->wb 184

This theorem is referenced by: pm5.41 364 orimdi 847 bnj1174 34059

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

This theorem depends on definitions: df-bi 185