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 513 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: anc2ri 557 pm5.31 826 fnun 6456 fco 6524 mapdom2 8676 fisupg 8754 fiint 8783 dffi3 8883 fiinfg 8951 dfac2b 9544 cflm 9660 cfslbn 9677 cardmin 9974 fpwwe2lem12 10051 fpwwe2lem13 10052 elfznelfzob 13131 modsumfzodifsn 13300 dvdsdivcl 15654 isprm5 16039 latjlej1 17663 latmlem1 17679 cnrest2 21822 cnpresti 21824 trufil 22446 stdbdxmet 23052 lgsdir 25835 elwwlks2 27672 orthin 29150 mdbr2 30000 dmdbr2 30007 mdsl2i 30026 atcvat4i 30101 mdsymlem3 30109 wzel 33008 ontgval 33676 poimirlem3 34776 poimirlem4 34777 poimirlem29 34802 poimir 34806 cmtbr4N 36271 cvrat4 36459 cdlemblem 36809 negexpidd 39157 3cubeslem1 39159 ensucne0OLD 39774 itschlc0xyqsol 44682 elpglem2 44742 |
Copyright terms: Public domain | W3C validator |