![]() |
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 410 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
3 | 3jcad.2 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜃)) | |
4 | 3 | imp 410 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | 3jcad.3 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜏)) | |
6 | 5 | imp 410 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
7 | 2, 4, 6 | 3jca 1125 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃 ∧ 𝜏)) |
8 | 7 | ex 416 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1084 |
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 210 df-an 400 df-3an 1086 |
This theorem is referenced by: onfununi 7961 uzm1 12264 ixxssixx 12740 iccid 12771 iccsplit 12863 fzen 12919 lmodprop2d 19689 fbun 22445 hausflim 22586 icoopnst 23544 iocopnst 23545 abelth 25036 usgr2pth 27553 shsvs 29106 cnlnssadj 29863 fnrelpredd 32472 cvmlift2lem10 32672 endofsegid 33659 elicc3 33778 areacirclem1 35145 islvol2aN 36888 alrim3con13v 41239 bgoldbtbndlem4 44326 |
Copyright terms: Public domain | W3C validator |