![]() |
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 206 df-an 396 |
This theorem is referenced by: dfmoeu 2522 mopick2 2625 2eu6 2644 cgsexg 3511 cgsex2g 3512 cgsex4g 3513 cgsex4gOLD 3514 cgsex4gOLDOLD 3515 ss2abdv 4052 reximdva0 4343 difsn 4793 preq12b 4843 elinxp 6009 ssrnres 6167 ordtr2 6398 elunirn 7242 fnoprabg 7523 tz7.49 8440 omord 8563 ficard 10556 fpwwe2lem11 10632 1idpr 11020 xrsupsslem 13283 xrinfmsslem 13284 fzospliti 13661 sqrt2irr 16189 algcvga 16513 prmind2 16619 infpn2 16845 grpinveu 18894 1stcrest 23279 fgss2 23700 fgcl 23704 filufint 23746 metrest 24355 reconnlem2 24665 plydivex 26151 ftalem3 26923 chtub 27061 lgsqrmodndvds 27202 2sqlem10 27277 dchrisum0flb 27359 pntpbnd1 27435 nolesgn2o 27520 nosupbnd1lem4 27560 noinfbnd1lem4 27575 noetalem1 27590 clwwlkn1loopb 29765 2pthfrgrrn2 30005 grpoidinvlem3 30228 grpoinveu 30241 elim2ifim 32246 iocinif 32461 qsxpid 32944 tpr2rico 33381 bnj168 34230 dfon2lem8 35257 nn0prpwlem 35697 bj-opelidres 36532 difunieq 36745 voliunnfl 37022 dalem20 39054 elpaddn0 39161 cdleme25a 39714 cdleme29ex 39735 cdlemefr29exN 39763 dibglbN 40527 dihlsscpre 40595 lcfl7N 40862 mapdh9a 41150 mapdh9aOLDN 41151 hdmap11lem2 41203 rtprmirr 41726 sqrtcval 42881 ax6e2eq 43807 eliin2f 44281 itschlc0xyqsol1 47640 mpbiran3d 47670 |
Copyright terms: Public domain | W3C validator |