![]() |
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 617 | 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 206 df-an 396 |
This theorem is referenced by: im2anan9r 620 anim12 806 trin 5277 somo 5625 xpss12 5691 f1oun 6852 poxp 8118 soxp 8119 brecop 8808 ingru 10814 genpss 11003 genpnnp 11004 tgcl 22693 txlm 23373 upgrpredgv 28667 3wlkdlem4 29683 frgrwopreglem5 29842 frgrwopreglem5ALT 29843 icorempo 36536 ax12eq 38115 ax12el 38116 odd2prm2 46685 |
Copyright terms: Public domain | W3C validator |