|   | 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 1128 | . 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 8382 uzm1 12917 ixxssixx 13402 iccid 13433 iccsplit 13526 fzen 13582 lmodprop2d 20923 fbun 23849 hausflim 23990 icoopnst 24970 iocopnst 24971 abelth 26486 usgr2pth 29785 shsvs 31343 cnlnssadj 32100 fnrelpredd 35104 cvmlift2lem10 35318 endofsegid 36087 elicc3 36319 areacirclem1 37716 islvol2aN 39595 alrim3con13v 44558 ormkglobd 46895 bgoldbtbndlem4 47800 | 
| Copyright terms: Public domain | W3C validator |