Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > jcab | Structured version Visualization version Unicode version |
Description: Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 27-Nov-2013.) |
Ref | Expression |
---|---|
jcab |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 473 | . . . 4 | |
2 | 1 | imim2i 16 | . . 3 |
3 | simpr 477 | . . . 4 | |
4 | 3 | imim2i 16 | . . 3 |
5 | 2, 4 | jca 554 | . 2 |
6 | pm3.43 906 | . 2 | |
7 | 5, 6 | impbii 199 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 |
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 197 df-an 386 |
This theorem is referenced by: ordi 908 pm4.76 910 pm5.44 950 2mo2 2550 ssconb 3743 ssin 3835 tfr3 7495 trclfvcotr 13750 isprm2 15395 lgsquad2lem2 25110 ostthlem2 25317 pclclN 35177 ifpbibib 37855 elmapintrab 37882 elinintrab 37883 2reu4a 41189 |
Copyright terms: Public domain | W3C validator |