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 444 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
3 | 3jcad.2 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜃)) | |
4 | 3 | imp 444 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | 3jcad.3 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜏)) | |
6 | 5 | imp 444 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
7 | 2, 4, 6 | 3jca 1235 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃 ∧ 𝜏)) |
8 | 7 | ex 449 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: onfununi 7325 uzm1 11594 ixxssixx 12060 iccid 12091 iccsplit 12176 fzen 12229 lmodprop2d 18748 fbun 21454 hausflim 21595 icoopnst 22546 iocopnst 22547 abelth 23999 eupai 26494 shsvs 27566 cnlnssadj 28323 cvmlift2lem10 30548 endofsegid 31362 elicc3 31481 areacirclem1 32670 islvol2aN 33896 alrim3con13v 37764 bgoldbtbndlem4 40224 usgr2pth 40970 |
Copyright terms: Public domain | W3C validator |