![]() |
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 | adantr 480 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜒)) |
3 | im2an9.2 | . . 3 ⊢ (𝜃 → (𝜏 → 𝜂)) | |
4 | 3 | adantl 481 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜏 → 𝜂)) |
5 | 2, 4 | anim12d 585 | 1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 385 |
This theorem is referenced by: im2anan9r 899 trin 4796 somo 5098 xpss12 5158 f1oun 6194 poxp 7334 soxp 7335 brecop 7883 ingru 9675 genpss 9864 genpnnp 9865 tgcl 20821 txlm 21499 upgrpredgv 26079 3wlkdlem4 27140 frgrwopreglem5 27301 frgrwopreglem5ALT 27302 icorempt2 33329 ax12eq 34545 ax12el 34546 odd2prm2 41952 |
Copyright terms: Public domain | W3C validator |