![]() |
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 511 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 206 df-an 395 |
This theorem is referenced by: anc2ri 555 pm5.31 829 fnun 6669 fcof 6746 fcoOLD 6748 mapdom2 9173 fisupg 9316 fiint 9350 dffi3 9456 fiinfg 9524 dfac2b 10155 nnadju 10222 cflm 10275 cfslbn 10292 cardmin 10589 fpwwe2lem11 10666 fpwwe2lem12 10667 elfznelfzob 13774 modsumfzodifsn 13945 dvdsdivcl 16296 isprm5 16681 latjlej1 18448 latmlem1 18464 cnrest2 23234 cnpresti 23236 trufil 23858 stdbdxmet 24468 lgsdir 27310 elwwlks2 29849 orthin 31328 mdbr2 32178 dmdbr2 32185 mdsl2i 32204 atcvat4i 32279 mdsymlem3 32287 wzel 35551 ontgval 36046 poimirlem3 37227 poimirlem4 37228 poimirlem29 37253 poimir 37257 cmtbr4N 38857 cvrat4 39046 cdlemblem 39396 negexpidd 42244 3cubeslem1 42246 tfsconcatb0 42915 ensucne0OLD 43102 gricer 47376 itschlc0xyqsol 48026 elpglem2 48329 |
Copyright terms: Public domain | W3C validator |