|   | 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 808 trin 5270 somo 5630 xpss12 5699 f1oun 6866 poxp 8154 soxp 8155 brecop 8851 dfac5lem4 10167 ingru 10856 genpss 11045 genpnnp 11046 tgcl 22977 txlm 23657 upgrpredgv 29157 3wlkdlem4 30182 frgrwopreglem5 30341 frgrwopreglem5ALT 30342 icorempo 37353 ax12eq 38943 ax12el 38944 odd2prm2 47710 | 
| Copyright terms: Public domain | W3C validator |