![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > im2anan9 | Structured version Visualization version GIF 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 | adantrd 492 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜒)) |
3 | im2an9.2 | . . 3 ⊢ (𝜃 → (𝜏 → 𝜂)) | |
4 | 3 | adantld 491 | . 2 ⊢ (𝜃 → ((𝜓 ∧ 𝜏) → 𝜂)) |
5 | 2, 4 | anim12ii 618 | 1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 206 df-an 397 |
This theorem is referenced by: im2anan9r 621 anim12 807 trin 5277 somo 5625 xpss12 5691 f1oun 6852 poxp 8116 soxp 8117 brecop 8806 ingru 10812 genpss 11001 genpnnp 11002 tgcl 22479 txlm 23159 upgrpredgv 28437 3wlkdlem4 29453 frgrwopreglem5 29612 frgrwopreglem5ALT 29613 icorempo 36318 ax12eq 37897 ax12el 37898 odd2prm2 46465 |
Copyright terms: Public domain | W3C validator |