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 5184 somo 5512 xpss12 5572 f1oun 6636 poxp 7824 soxp 7825 brecop 8392 ingru 10239 genpss 10428 genpnnp 10429 tgcl 21579 txlm 22258 upgrpredgv 26926 3wlkdlem4 27943 frgrwopreglem5 28102 frgrwopreglem5ALT 28103 icorempo 34634 ax12eq 36079 ax12el 36080 odd2prm2 43890 |
Copyright terms: Public domain | W3C validator |