![]() |
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 505 | 1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 |
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 388 |
This theorem is referenced by: dfmoeu 2547 mopick2 2675 2eu6 2697 cgsexg 3460 cgsex2g 3461 cgsex4g 3462 reximdva0 4201 difsn 4610 preq12b 4660 elinxp 5740 ssrnres 5880 ordtr2 6078 elunirn 6841 fnoprabg 7097 tz7.49 7890 omord 8001 ficard 9791 fpwwe2lem12 9867 1idpr 10255 xrsupsslem 12522 xrinfmsslem 12523 fzospliti 12890 sqrt2irr 15468 algcvga 15785 prmind2 15891 infpn2 16111 grpinveu 17937 1stcrest 21780 fgss2 22201 fgcl 22205 filufint 22247 metrest 22852 reconnlem2 23153 plydivex 24604 ftalem3 25369 chtub 25505 lgsqrmodndvds 25646 2sqlem10 25721 dchrisum0flb 25803 pntpbnd1 25879 clwwlkn1loopb 27574 2pthfrgrrn2 27832 grpoidinvlem3 28075 grpoinveu 28088 elim2ifim 30085 iocinif 30280 tpr2rico 30831 bnj168 31680 dfon2lem8 32595 dftrpred3g 32633 nolesgn2o 32739 nosupbnd1lem4 32772 nn0prpwlem 33231 difunieq 34137 voliunnfl 34417 dalem20 36314 elpaddn0 36421 cdleme25a 36974 cdleme29ex 36995 cdlemefr29exN 37023 dibglbN 37787 dihlsscpre 37855 lcfl7N 38122 mapdh9a 38410 mapdh9aOLDN 38411 hdmap11lem2 38463 rtprmirr 38667 ax6e2eq 40350 eliin2f 40831 itschlc0xyqsol1 44156 |
Copyright terms: Public domain | W3C validator |