![]() |
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 491 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜒)) |
3 | im2an9.2 | . . 3 ⊢ (𝜃 → (𝜏 → 𝜂)) | |
4 | 3 | adantld 490 | . 2 ⊢ (𝜃 → ((𝜓 ∧ 𝜏) → 𝜂)) |
5 | 2, 4 | anim12ii 618 | 1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 |
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 207 df-an 396 |
This theorem is referenced by: im2anan9r 621 anim12 809 trin 5277 somo 5635 xpss12 5704 f1oun 6868 poxp 8152 soxp 8153 brecop 8849 dfac5lem4 10164 ingru 10853 genpss 11042 genpnnp 11043 tgcl 22992 txlm 23672 upgrpredgv 29171 3wlkdlem4 30191 frgrwopreglem5 30350 frgrwopreglem5ALT 30351 icorempo 37334 ax12eq 38923 ax12el 38924 odd2prm2 47643 |
Copyright terms: Public domain | W3C validator |