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 516 | 1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: dfmoeu 2535 mopick2 2638 2eu6 2657 cgsexg 3450 cgsex2g 3451 cgsex4g 3452 cgsex4gOLD 3453 ss2abdv 3977 reximdva0 4266 difsn 4711 preq12b 4761 elinxp 5889 ssrnres 6041 ordtr2 6257 elunirn 7064 fnoprabg 7333 tz7.49 8181 omord 8296 dftrpred3g 9339 ficard 10179 fpwwe2lem11 10255 1idpr 10643 xrsupsslem 12897 xrinfmsslem 12898 fzospliti 13274 sqrt2irr 15810 algcvga 16136 prmind2 16242 infpn2 16466 grpinveu 18402 1stcrest 22350 fgss2 22771 fgcl 22775 filufint 22817 metrest 23422 reconnlem2 23724 plydivex 25190 ftalem3 25957 chtub 26093 lgsqrmodndvds 26234 2sqlem10 26309 dchrisum0flb 26391 pntpbnd1 26467 clwwlkn1loopb 28126 2pthfrgrrn2 28366 grpoidinvlem3 28587 grpoinveu 28600 elim2ifim 30607 iocinif 30822 qsxpid 31272 tpr2rico 31576 bnj168 32421 dfon2lem8 33485 nolesgn2o 33611 nosupbnd1lem4 33651 noinfbnd1lem4 33666 noetalem1 33681 nn0prpwlem 34248 bj-opelidres 35067 difunieq 35282 voliunnfl 35558 dalem20 37444 elpaddn0 37551 cdleme25a 38104 cdleme29ex 38125 cdlemefr29exN 38153 dibglbN 38917 dihlsscpre 38985 lcfl7N 39252 mapdh9a 39540 mapdh9aOLDN 39541 hdmap11lem2 39593 rtprmirr 40055 sqrtcval 40925 ax6e2eq 41850 eliin2f 42327 itschlc0xyqsol1 45785 mpbiran3d 45815 |
Copyright terms: Public domain | W3C validator |