![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > jctild | Structured version Visualization version GIF version |
Description: Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.) |
Ref | Expression |
---|---|
jctild.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
jctild.2 | ⊢ (𝜑 → 𝜃) |
Ref | Expression |
---|---|
jctild | ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jctild.2 | . . 3 ⊢ (𝜑 → 𝜃) | |
2 | 1 | a1d 25 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
3 | jctild.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
4 | 2, 3 | jcad 510 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: anc2li 553 syl6an 676 ordunidif 6011 isofrlem 6845 dfwe2 7242 orduniorsuc 7291 poxp 7553 fnse 7558 ssenen 8403 dffi3 8606 fpwwe2lem13 9779 zmulcl 11754 rpneg 12146 rexuz3 14465 cau3lem 14471 climrlim2 14655 o1rlimmul 14726 iseralt 14792 gcdzeq 15644 isprm3 15768 vdwnnlem2 16071 ablfaclem3 18840 epttop 21184 lmcnp 21479 dfconn2 21593 txcnp 21794 cmphaushmeo 21974 isfild 22032 cnpflf2 22174 flimfnfcls 22202 alexsubALT 22225 fgcfil 23439 bcthlem5 23496 ivthlem2 23618 ivthlem3 23619 dvfsumrlim 24193 plypf1 24367 axeuclidlem 26261 usgr2wlkneq 27058 wwlksnredwwlkn0 27209 wwlksnredwwlkn0OLD 27210 wwlksnextwrd 27211 wwlksnextwrdOLD 27216 clwlkclwwlklem2a1 27321 lnon0 28208 hstles 29645 mdsl1i 29735 atcveq0 29762 atcvat4i 29811 cdjreui 29846 issgon 30731 connpconn 31763 tfisg 32254 frpoinsg 32280 frmin 32281 outsideofrflx 32773 isbasisrelowllem1 33748 isbasisrelowllem2 33749 poimirlem3 33956 poimirlem29 33982 poimir 33986 heicant 33988 equivtotbnd 34119 ismtybndlem 34147 cvrat4 35518 linepsubN 35827 pmapsub 35843 osumcllem4N 36034 pexmidlem1N 36045 dochexmidlem1 37535 clcnvlem 38771 2reu1 42011 iccpartimp 42241 sbgoldbwt 42495 sbgoldbst 42496 elsetrecslem 43340 |
Copyright terms: Public domain | W3C validator |