| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > jctird | Structured version Visualization version GIF version | ||
| Description: Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.) |
| Ref | Expression |
|---|---|
| jctird.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| jctird.2 | ⊢ (𝜑 → 𝜃) |
| Ref | Expression |
|---|---|
| jctird | ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | jctird.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | jctird.2 | . . 3 ⊢ (𝜑 → 𝜃) | |
| 3 | 2 | a1d 25 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
| 4 | 1, 3 | jcad 512 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 |
| This theorem is referenced by: anc2ri 556 pm5.31 831 fnun 6682 fcof 6759 brinxper 8774 mapdom2 9188 fisupg 9324 fiint 9366 fiintOLD 9367 dffi3 9471 fiinfg 9539 dfac2b 10171 nnadju 10238 cflm 10290 cfslbn 10307 cardmin 10604 fpwwe2lem11 10681 fpwwe2lem12 10682 elfznelfzob 13812 modsumfzodifsn 13985 dvdsdivcl 16353 isprm5 16744 latjlej1 18498 latmlem1 18514 cnrest2 23294 cnpresti 23296 trufil 23918 stdbdxmet 24528 lgsdir 27376 elwwlks2 29986 orthin 31465 mdbr2 32315 dmdbr2 32322 mdsl2i 32341 atcvat4i 32416 mdsymlem3 32424 wzel 35825 ontgval 36432 poimirlem3 37630 poimirlem4 37631 poimirlem29 37656 poimir 37660 cmtbr4N 39256 cvrat4 39445 cdlemblem 39795 negexpidd 42693 3cubeslem1 42695 tfsconcatb0 43357 ensucne0OLD 43543 itschlc0xyqsol 48688 elpglem2 49231 |
| Copyright terms: Public domain | W3C validator |