![]() |
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 406 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
3 | 3jcad.2 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜃)) | |
4 | 3 | imp 406 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | 3jcad.3 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜏)) | |
6 | 5 | imp 406 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) |
7 | 2, 4, 6 | 3jca 1127 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃 ∧ 𝜏)) |
8 | 7 | ex 412 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 df-3an 1088 |
This theorem is referenced by: onfununi 8380 uzm1 12914 ixxssixx 13398 iccid 13429 iccsplit 13522 fzen 13578 lmodprop2d 20939 fbun 23864 hausflim 24005 icoopnst 24983 iocopnst 24984 abelth 26500 usgr2pth 29797 shsvs 31352 cnlnssadj 32109 fnrelpredd 35082 cvmlift2lem10 35297 endofsegid 36067 elicc3 36300 areacirclem1 37695 islvol2aN 39575 alrim3con13v 44531 bgoldbtbndlem4 47733 |
Copyright terms: Public domain | W3C validator |