| 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 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: anc2li 555 equvini 2460 2reu1 3897 frpoinsg 6364 ordunidif 6433 isofrlem 7360 dfwe2 7794 orduniorsuc 7850 tfisg 7875 poxp 8153 fnse 8158 ssenen 9191 dffi3 9471 fpwwe2lem12 10682 zmulcl 12666 rpneg 13067 rexuz3 15387 cau3lem 15393 climrlim2 15583 o1rlimmul 15655 iseralt 15721 gcdzeq 16589 isprm3 16720 vdwnnlem2 17034 ablfaclem3 20107 epttop 23016 lmcnp 23312 dfconn2 23427 txcnp 23628 cmphaushmeo 23808 isfild 23866 cnpflf2 24008 flimfnfcls 24036 alexsubALT 24059 fgcfil 25305 bcthlem5 25362 ivthlem2 25487 ivthlem3 25488 dvfsumrlim 26072 plypf1 26251 noetalem1 27786 noseqinds 28299 axeuclidlem 28977 usgr2wlkneq 29776 wwlksnredwwlkn0 29916 wwlksnextwrd 29917 clwlkclwwlklem2a1 30011 lnon0 30817 hstles 32250 mdsl1i 32340 atcveq0 32367 atcvat4i 32416 cdjreui 32451 issgon 34124 connpconn 35240 outsideofrflx 36128 isbasisrelowllem1 37356 isbasisrelowllem2 37357 poimirlem3 37630 poimirlem29 37656 poimir 37660 heicant 37662 equivtotbnd 37785 ismtybndlem 37813 cvrat4 39445 linepsubN 39754 pmapsub 39770 osumcllem4N 39961 pexmidlem1N 39972 dochexmidlem1 41462 cantnfresb 43337 harval3 43551 clcnvlem 43636 relpfrlem 44974 iccpartimp 47404 sbgoldbwt 47764 sbgoldbst 47765 elsetrecslem 49218 |
| Copyright terms: Public domain | W3C validator |