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 409 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
3 | 3jcad.2 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜃)) | |
4 | 3 | imp 409 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | 3jcad.3 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜏)) | |
6 | 5 | imp 409 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
7 | 2, 4, 6 | 3jca 1124 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃 ∧ 𝜏)) |
8 | 7 | ex 415 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 |
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 df-3an 1085 |
This theorem is referenced by: onfununi 7978 uzm1 12277 ixxssixx 12753 iccid 12784 iccsplit 12872 fzen 12925 lmodprop2d 19696 fbun 22448 hausflim 22589 icoopnst 23543 iocopnst 23544 abelth 25029 usgr2pth 27545 shsvs 29100 cnlnssadj 29857 cvmlift2lem10 32559 endofsegid 33546 elicc3 33665 areacirclem1 34997 islvol2aN 36743 alrim3con13v 40887 bgoldbtbndlem4 43993 |
Copyright terms: Public domain | W3C validator |