Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > im2anan9 | Structured version Visualization version Unicode version |
Description: Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.) |
Ref | Expression |
---|---|
im2an9.1 | |
im2an9.2 |
Ref | Expression |
---|---|
im2anan9 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | im2an9.1 | . . 3 | |
2 | 1 | adantr 481 | . 2 |
3 | im2an9.2 | . . 3 | |
4 | 3 | adantl 482 | . 2 |
5 | 2, 4 | anim12d 586 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 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: im2anan9r 881 trin 4763 somo 5069 xpss12 5225 f1oun 6156 poxp 7289 soxp 7290 brecop 7840 ingru 9637 genpss 9826 genpnnp 9827 tgcl 20773 txlm 21451 upgrpredgv 26034 3wlkdlem4 27022 frgrwopreglem5 27185 frgrwopreglem5ALT 27186 icorempt2 33199 ax12eq 34226 ax12el 34227 odd2prm2 41627 |
Copyright terms: Public domain | W3C validator |