![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3jcad | Structured version Visualization version GIF version |
Description: Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.) |
Ref | Expression |
---|---|
3jcad.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
3jcad.2 | ⊢ (𝜑 → (𝜓 → 𝜃)) |
3jcad.3 | ⊢ (𝜑 → (𝜓 → 𝜏)) |
Ref | Expression |
---|---|
3jcad | ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3jcad.1 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | imp 407 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
3 | 3jcad.2 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜃)) | |
4 | 3 | imp 407 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | 3jcad.3 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜏)) | |
6 | 5 | imp 407 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
7 | 2, 4, 6 | 3jca 1128 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃 ∧ 𝜏)) |
8 | 7 | ex 413 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 |
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 397 df-3an 1089 |
This theorem is referenced by: onfununi 8340 uzm1 12859 ixxssixx 13337 iccid 13368 iccsplit 13461 fzen 13517 lmodprop2d 20533 fbun 23343 hausflim 23484 icoopnst 24454 iocopnst 24455 abelth 25952 usgr2pth 29018 shsvs 30571 cnlnssadj 31328 fnrelpredd 34087 cvmlift2lem10 34298 endofsegid 35052 elicc3 35197 areacirclem1 36571 islvol2aN 38458 alrim3con13v 43284 bgoldbtbndlem4 46466 |
Copyright terms: Public domain | W3C validator |