| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ancld | Structured version Visualization version GIF version | ||
| Description: Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.) |
| Ref | Expression |
|---|---|
| ancld.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| Ref | Expression |
|---|---|
| ancld | ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | idd 24 | . 2 ⊢ (𝜑 → (𝜓 → 𝜓)) | |
| 2 | ancld.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 3 | 1, 2 | 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: dfmoeu 2536 mopick2 2637 2eu6 2657 cgsexg 3526 cgsex2g 3527 cgsex4g 3528 cgsex4gOLD 3529 reximdva0 4355 difsn 4798 preq12b 4850 elinxp 6037 ssrnres 6198 ordtr2 6428 elunirn 7271 fnoprabg 7556 tz7.49 8485 omord 8606 ficard 10605 fpwwe2lem11 10681 1idpr 11069 xrsupsslem 13349 xrinfmsslem 13350 fzospliti 13731 sqrt2irr 16285 algcvga 16616 prmind2 16722 infpn2 16951 grpinveu 18992 1stcrest 23461 fgss2 23882 fgcl 23886 filufint 23928 metrest 24537 reconnlem2 24849 plydivex 26339 rtprmirr 26803 ftalem3 27118 chtub 27256 lgsqrmodndvds 27397 2sqlem10 27472 dchrisum0flb 27554 pntpbnd1 27630 nolesgn2o 27716 nosupbnd1lem4 27756 noinfbnd1lem4 27771 noetalem1 27786 clwwlkn1loopb 30062 2pthfrgrrn2 30302 grpoidinvlem3 30525 grpoinveu 30538 elim2ifim 32558 iocinif 32783 qsxpid 33390 tpr2rico 33911 bnj168 34744 ellcsrspsn 35646 dfon2lem8 35791 nn0prpwlem 36323 bj-opelidres 37162 difunieq 37375 voliunnfl 37671 dalem20 39695 elpaddn0 39802 cdleme25a 40355 cdleme29ex 40376 cdlemefr29exN 40404 dibglbN 41168 dihlsscpre 41236 lcfl7N 41503 mapdh9a 41791 mapdh9aOLDN 41792 hdmap11lem2 41844 eu6w 42686 sqrtcval 43654 ax6e2eq 44577 eliin2f 45109 clnbgr3stgrgrlic 47979 itschlc0xyqsol1 48687 mpbiran3d 48717 |
| Copyright terms: Public domain | W3C validator |