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 494 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜒)) |
3 | im2an9.2 | . . 3 ⊢ (𝜃 → (𝜏 → 𝜂)) | |
4 | 3 | adantld 493 | . 2 ⊢ (𝜃 → ((𝜓 ∧ 𝜏) → 𝜂)) |
5 | 2, 4 | anim12ii 619 | 1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: im2anan9r 622 anim12 807 trin 5174 somo 5504 xpss12 5564 f1oun 6628 poxp 7816 soxp 7817 brecop 8384 ingru 10231 genpss 10420 genpnnp 10421 tgcl 21571 txlm 22250 upgrpredgv 26918 3wlkdlem4 27935 frgrwopreglem5 28094 frgrwopreglem5ALT 28095 icorempo 34626 ax12eq 36071 ax12el 36072 odd2prm2 43877 |
Copyright terms: Public domain | W3C validator |